Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  enq0tr Structured version   GIF version

Theorem enq0tr 6283
 Description: The equivalence relation for non-negative fractions is transitive. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
Assertion
Ref Expression
enq0tr ((f ~Q0 g g ~Q0 ) → f ~Q0 )

Proof of Theorem enq0tr
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑠 𝑡 u v w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2534 . . . . . . . . . 10 f V
2 vex 2534 . . . . . . . . . 10 g V
3 eleq1 2078 . . . . . . . . . . . 12 (x = f → (x (𝜔 × N) ↔ f (𝜔 × N)))
43anbi1d 441 . . . . . . . . . . 11 (x = f → ((x (𝜔 × N) y (𝜔 × N)) ↔ (f (𝜔 × N) y (𝜔 × N))))
5 eqeq1 2024 . . . . . . . . . . . . . 14 (x = f → (x = ⟨z, w⟩ ↔ f = ⟨z, w⟩))
65anbi1d 441 . . . . . . . . . . . . 13 (x = f → ((x = ⟨z, w y = ⟨v, u⟩) ↔ (f = ⟨z, w y = ⟨v, u⟩)))
76anbi1d 441 . . . . . . . . . . . 12 (x = f → (((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
874exbidv 1728 . . . . . . . . . . 11 (x = f → (zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ zwvu((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
94, 8anbi12d 445 . . . . . . . . . 10 (x = f → (((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((f (𝜔 × N) y (𝜔 × N)) zwvu((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))))
10 eleq1 2078 . . . . . . . . . . . 12 (y = g → (y (𝜔 × N) ↔ g (𝜔 × N)))
1110anbi2d 440 . . . . . . . . . . 11 (y = g → ((f (𝜔 × N) y (𝜔 × N)) ↔ (f (𝜔 × N) g (𝜔 × N))))
12 eqeq1 2024 . . . . . . . . . . . . . 14 (y = g → (y = ⟨v, u⟩ ↔ g = ⟨v, u⟩))
1312anbi2d 440 . . . . . . . . . . . . 13 (y = g → ((f = ⟨z, w y = ⟨v, u⟩) ↔ (f = ⟨z, w g = ⟨v, u⟩)))
1413anbi1d 441 . . . . . . . . . . . 12 (y = g → (((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
15144exbidv 1728 . . . . . . . . . . 11 (y = g → (zwvu((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
1611, 15anbi12d 445 . . . . . . . . . 10 (y = g → (((f (𝜔 × N) y (𝜔 × N)) zwvu((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))))
17 df-enq0 6273 . . . . . . . . . 10 ~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))}
181, 2, 9, 16, 17brab 3979 . . . . . . . . 9 (f ~Q0 g ↔ ((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
19 vex 2534 . . . . . . . . . 10 V
20 eleq1 2078 . . . . . . . . . . . 12 (x = g → (x (𝜔 × N) ↔ g (𝜔 × N)))
2120anbi1d 441 . . . . . . . . . . 11 (x = g → ((x (𝜔 × N) y (𝜔 × N)) ↔ (g (𝜔 × N) y (𝜔 × N))))
22 eqeq1 2024 . . . . . . . . . . . . . 14 (x = g → (x = ⟨𝑎, 𝑏⟩ ↔ g = ⟨𝑎, 𝑏⟩))
2322anbi1d 441 . . . . . . . . . . . . 13 (x = g → ((x = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) ↔ (g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩)))
2423anbi1d 441 . . . . . . . . . . . 12 (x = g → (((x = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ ((g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
25244exbidv 1728 . . . . . . . . . . 11 (x = g → (𝑎𝑏𝑠𝑡((x = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
2621, 25anbi12d 445 . . . . . . . . . 10 (x = g → (((x (𝜔 × N) y (𝜔 × N)) 𝑎𝑏𝑠𝑡((x = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) ↔ ((g (𝜔 × N) y (𝜔 × N)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
27 eleq1 2078 . . . . . . . . . . . 12 (y = → (y (𝜔 × N) ↔ (𝜔 × N)))
2827anbi2d 440 . . . . . . . . . . 11 (y = → ((g (𝜔 × N) y (𝜔 × N)) ↔ (g (𝜔 × N) (𝜔 × N))))
29 eqeq1 2024 . . . . . . . . . . . . . 14 (y = → (y = ⟨𝑠, 𝑡⟩ ↔ = ⟨𝑠, 𝑡⟩))
3029anbi2d 440 . . . . . . . . . . . . 13 (y = → ((g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) ↔ (g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩)))
3130anbi1d 441 . . . . . . . . . . . 12 (y = → (((g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
32314exbidv 1728 . . . . . . . . . . 11 (y = → (𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
3328, 32anbi12d 445 . . . . . . . . . 10 (y = → (((g (𝜔 × N) y (𝜔 × N)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) ↔ ((g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
34 df-enq0 6273 . . . . . . . . . 10 ~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) 𝑎𝑏𝑠𝑡((x = ⟨𝑎, 𝑏 y = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))}
352, 19, 26, 33, 34brab 3979 . . . . . . . . 9 (g ~Q0 ↔ ((g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
3618, 35anbi12i 436 . . . . . . . 8 ((f ~Q0 g g ~Q0 ) ↔ (((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ((g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
3736biimpi 113 . . . . . . 7 ((f ~Q0 g g ~Q0 ) → (((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ((g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
38 an4 507 . . . . . . 7 ((((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ((g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ (((f (𝜔 × N) g (𝜔 × N)) (g (𝜔 × N) (𝜔 × N))) (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
3937, 38sylib 127 . . . . . 6 ((f ~Q0 g g ~Q0 ) → (((f (𝜔 × N) g (𝜔 × N)) (g (𝜔 × N) (𝜔 × N))) (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
40 3anass 875 . . . . . . . 8 ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) ↔ (f (𝜔 × N) (g (𝜔 × N) (𝜔 × N))))
41 anass 383 . . . . . . . . 9 (((f (𝜔 × N) g (𝜔 × N)) (g (𝜔 × N) (𝜔 × N))) ↔ (f (𝜔 × N) (g (𝜔 × N) (g (𝜔 × N) (𝜔 × N)))))
42 anass 383 . . . . . . . . . 10 (((g (𝜔 × N) g (𝜔 × N)) (𝜔 × N)) ↔ (g (𝜔 × N) (g (𝜔 × N) (𝜔 × N))))
4342anbi2i 433 . . . . . . . . 9 ((f (𝜔 × N) ((g (𝜔 × N) g (𝜔 × N)) (𝜔 × N))) ↔ (f (𝜔 × N) (g (𝜔 × N) (g (𝜔 × N) (𝜔 × N)))))
44 anidm 376 . . . . . . . . . . 11 ((g (𝜔 × N) g (𝜔 × N)) ↔ g (𝜔 × N))
4544anbi1i 434 . . . . . . . . . 10 (((g (𝜔 × N) g (𝜔 × N)) (𝜔 × N)) ↔ (g (𝜔 × N) (𝜔 × N)))
4645anbi2i 433 . . . . . . . . 9 ((f (𝜔 × N) ((g (𝜔 × N) g (𝜔 × N)) (𝜔 × N))) ↔ (f (𝜔 × N) (g (𝜔 × N) (𝜔 × N))))
4741, 43, 463bitr2i 197 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N)) (g (𝜔 × N) (𝜔 × N))) ↔ (f (𝜔 × N) (g (𝜔 × N) (𝜔 × N))))
4840, 47bitr4i 176 . . . . . . 7 ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) ↔ ((f (𝜔 × N) g (𝜔 × N)) (g (𝜔 × N) (𝜔 × N))))
4948anbi1i 434 . . . . . 6 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ (((f (𝜔 × N) g (𝜔 × N)) (g (𝜔 × N) (𝜔 × N))) (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5039, 49sylibr 137 . . . . 5 ((f ~Q0 g g ~Q0 ) → ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
51 ee8anv 1788 . . . . . 6 (zwvu𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) ↔ (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
5251anbi2i 433 . . . . 5 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) zwvu𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) 𝑎𝑏𝑠𝑡((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5350, 52sylibr 137 . . . 4 ((f ~Q0 g g ~Q0 ) → ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) zwvu𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
54 19.42vvvv 1768 . . . . . . 7 (𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
55542exbii 1475 . . . . . 6 (vu𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ vu((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
56552exbii 1475 . . . . 5 (zwvu𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ zwvu((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
57 19.42vvvv 1768 . . . . 5 (zwvu((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) 𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) zwvu𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5856, 57bitri 173 . . . 4 (zwvu𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) zwvu𝑎𝑏𝑠𝑡(((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5953, 58sylibr 137 . . 3 ((f ~Q0 g g ~Q0 ) → zwvu𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
60 3simpb 888 . . . . . . . . 9 ((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) → (f (𝜔 × N) (𝜔 × N)))
6160adantr 261 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (f (𝜔 × N) (𝜔 × N)))
62 simplll 473 . . . . . . . . . 10 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → f = ⟨z, w⟩)
63 simprlr 478 . . . . . . . . . 10 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → = ⟨𝑠, 𝑡⟩)
6462, 63jca 290 . . . . . . . . 9 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (f = ⟨z, w = ⟨𝑠, 𝑡⟩))
6564adantl 262 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (f = ⟨z, w = ⟨𝑠, 𝑡⟩))
66 oveq1 5439 . . . . . . . . . . . . . . . 16 (v = ∅ → (v ·𝑜 𝑡) = (∅ ·𝑜 𝑡))
6763adantl 262 . . . . . . . . . . . . . . . . . . . . . 22 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → = ⟨𝑠, 𝑡⟩)
68 simpl3 895 . . . . . . . . . . . . . . . . . . . . . 22 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝜔 × N))
6967, 68eqeltrrd 2093 . . . . . . . . . . . . . . . . . . . . 21 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ⟨𝑠, 𝑡 (𝜔 × N))
70 opelxp 4297 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑠, 𝑡 (𝜔 × N) ↔ (𝑠 𝜔 𝑡 N))
7169, 70sylib 127 . . . . . . . . . . . . . . . . . . . 20 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 𝜔 𝑡 N))
7271simprd 107 . . . . . . . . . . . . . . . . . . 19 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑡 N)
73 pinn 6163 . . . . . . . . . . . . . . . . . . 19 (𝑡 N𝑡 𝜔)
7472, 73syl 14 . . . . . . . . . . . . . . . . . 18 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑡 𝜔)
75 nnm0r 5969 . . . . . . . . . . . . . . . . . 18 (𝑡 𝜔 → (∅ ·𝑜 𝑡) = ∅)
7674, 75syl 14 . . . . . . . . . . . . . . . . 17 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (∅ ·𝑜 𝑡) = ∅)
7776eqeq2d 2029 . . . . . . . . . . . . . . . 16 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((v ·𝑜 𝑡) = (∅ ·𝑜 𝑡) ↔ (v ·𝑜 𝑡) = ∅))
7866, 77syl5ib 143 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (v ·𝑜 𝑡) = ∅))
79 simprr 472 . . . . . . . . . . . . . . . . . 18 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))
80 eqtr2 2036 . . . . . . . . . . . . . . . . . . . . . 22 ((g = ⟨v, u g = ⟨𝑎, 𝑏⟩) → ⟨v, u⟩ = ⟨𝑎, 𝑏⟩)
81 vex 2534 . . . . . . . . . . . . . . . . . . . . . . 23 v V
82 vex 2534 . . . . . . . . . . . . . . . . . . . . . . 23 u V
8381, 82opth 3944 . . . . . . . . . . . . . . . . . . . . . 22 (⟨v, u⟩ = ⟨𝑎, 𝑏⟩ ↔ (v = 𝑎 u = 𝑏))
8480, 83sylib 127 . . . . . . . . . . . . . . . . . . . . 21 ((g = ⟨v, u g = ⟨𝑎, 𝑏⟩) → (v = 𝑎 u = 𝑏))
85 oveq1 5439 . . . . . . . . . . . . . . . . . . . . . 22 (v = 𝑎 → (v ·𝑜 𝑡) = (𝑎 ·𝑜 𝑡))
86 oveq1 5439 . . . . . . . . . . . . . . . . . . . . . 22 (u = 𝑏 → (u ·𝑜 𝑠) = (𝑏 ·𝑜 𝑠))
8785, 86eqeqan12d 2033 . . . . . . . . . . . . . . . . . . . . 21 ((v = 𝑎 u = 𝑏) → ((v ·𝑜 𝑡) = (u ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
8884, 87syl 14 . . . . . . . . . . . . . . . . . . . 20 ((g = ⟨v, u g = ⟨𝑎, 𝑏⟩) → ((v ·𝑜 𝑡) = (u ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
8988ad2ant2lr 467 . . . . . . . . . . . . . . . . . . 19 (((f = ⟨z, w g = ⟨v, u⟩) (g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩)) → ((v ·𝑜 𝑡) = (u ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
9089ad2ant2r 466 . . . . . . . . . . . . . . . . . 18 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → ((v ·𝑜 𝑡) = (u ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
9179, 90mpbird 156 . . . . . . . . . . . . . . . . 17 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (v ·𝑜 𝑡) = (u ·𝑜 𝑠))
9291eqeq1d 2026 . . . . . . . . . . . . . . . 16 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → ((v ·𝑜 𝑡) = ∅ ↔ (u ·𝑜 𝑠) = ∅))
9392adantl 262 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((v ·𝑜 𝑡) = ∅ ↔ (u ·𝑜 𝑠) = ∅))
9478, 93sylibd 138 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (u ·𝑜 𝑠) = ∅))
95 simpllr 474 . . . . . . . . . . . . . . . . . . . 20 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → g = ⟨v, u⟩)
9695adantl 262 . . . . . . . . . . . . . . . . . . 19 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → g = ⟨v, u⟩)
97 simpl2 894 . . . . . . . . . . . . . . . . . . 19 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → g (𝜔 × N))
9896, 97eqeltrrd 2093 . . . . . . . . . . . . . . . . . 18 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ⟨v, u (𝜔 × N))
99 opelxp 4297 . . . . . . . . . . . . . . . . . 18 (⟨v, u (𝜔 × N) ↔ (v 𝜔 u N))
10098, 99sylib 127 . . . . . . . . . . . . . . . . 17 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v 𝜔 u N))
101100simprd 107 . . . . . . . . . . . . . . . 16 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → u N)
102 pinn 6163 . . . . . . . . . . . . . . . 16 (u Nu 𝜔)
103101, 102syl 14 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → u 𝜔)
10471simpld 105 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑠 𝜔)
105 nnm00 6009 . . . . . . . . . . . . . . 15 ((u 𝜔 𝑠 𝜔) → ((u ·𝑜 𝑠) = ∅ ↔ (u = ∅ 𝑠 = ∅)))
106103, 104, 105syl2anc 393 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((u ·𝑜 𝑠) = ∅ ↔ (u = ∅ 𝑠 = ∅)))
10794, 106sylibd 138 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (u = ∅ 𝑠 = ∅)))
108 elni2 6168 . . . . . . . . . . . . . . . 16 (u N ↔ (u 𝜔 u))
109108simprbi 260 . . . . . . . . . . . . . . 15 (u N → ∅ u)
110101, 109syl 14 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ∅ u)
111 n0i 3202 . . . . . . . . . . . . . 14 (∅ u → ¬ u = ∅)
112 biorf 650 . . . . . . . . . . . . . 14 u = ∅ → (𝑠 = ∅ ↔ (u = ∅ 𝑠 = ∅)))
113110, 111, 1123syl 17 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 = ∅ ↔ (u = ∅ 𝑠 = ∅)))
114107, 113sylibrd 158 . . . . . . . . . . . 12 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → 𝑠 = ∅))
11562adantl 262 . . . . . . . . . . . . . . . . . 18 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → f = ⟨z, w⟩)
116 simpl1 893 . . . . . . . . . . . . . . . . . 18 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → f (𝜔 × N))
117115, 116eqeltrrd 2093 . . . . . . . . . . . . . . . . 17 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ⟨z, w (𝜔 × N))
118 opelxp 4297 . . . . . . . . . . . . . . . . 17 (⟨z, w (𝜔 × N) ↔ (z 𝜔 w N))
119117, 118sylib 127 . . . . . . . . . . . . . . . 16 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z 𝜔 w N))
120119simprd 107 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → w N)
121 pinn 6163 . . . . . . . . . . . . . . 15 (w Nw 𝜔)
122120, 121syl 14 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → w 𝜔)
123 nnm0 5965 . . . . . . . . . . . . . 14 (w 𝜔 → (w ·𝑜 ∅) = ∅)
124122, 123syl 14 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (w ·𝑜 ∅) = ∅)
125 oveq2 5440 . . . . . . . . . . . . . 14 (𝑠 = ∅ → (w ·𝑜 𝑠) = (w ·𝑜 ∅))
126125eqeq1d 2026 . . . . . . . . . . . . 13 (𝑠 = ∅ → ((w ·𝑜 𝑠) = ∅ ↔ (w ·𝑜 ∅) = ∅))
127124, 126syl5ibrcom 146 . . . . . . . . . . . 12 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 = ∅ → (w ·𝑜 𝑠) = ∅))
128114, 127syld 40 . . . . . . . . . . 11 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (w ·𝑜 𝑠) = ∅))
129 oveq2 5440 . . . . . . . . . . . . . . . 16 (v = ∅ → (w ·𝑜 v) = (w ·𝑜 ∅))
130124eqeq2d 2029 . . . . . . . . . . . . . . . 16 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((w ·𝑜 v) = (w ·𝑜 ∅) ↔ (w ·𝑜 v) = ∅))
131129, 130syl5ib 143 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (w ·𝑜 v) = ∅))
132 simprlr 478 . . . . . . . . . . . . . . . 16 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z ·𝑜 u) = (w ·𝑜 v))
133132eqeq1d 2026 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((z ·𝑜 u) = ∅ ↔ (w ·𝑜 v) = ∅))
134131, 133sylibrd 158 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (z ·𝑜 u) = ∅))
135119simpld 105 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → z 𝜔)
136 nnm00 6009 . . . . . . . . . . . . . . 15 ((z 𝜔 u 𝜔) → ((z ·𝑜 u) = ∅ ↔ (z = ∅ u = ∅)))
137135, 103, 136syl2anc 393 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((z ·𝑜 u) = ∅ ↔ (z = ∅ u = ∅)))
138134, 137sylibd 138 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (z = ∅ u = ∅)))
139 biorf 650 . . . . . . . . . . . . . . 15 u = ∅ → (z = ∅ ↔ (u = ∅ z = ∅)))
140 orcom 634 . . . . . . . . . . . . . . 15 ((u = ∅ z = ∅) ↔ (z = ∅ u = ∅))
141139, 140syl6bb 185 . . . . . . . . . . . . . 14 u = ∅ → (z = ∅ ↔ (z = ∅ u = ∅)))
142110, 111, 1413syl 17 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z = ∅ ↔ (z = ∅ u = ∅)))
143138, 142sylibrd 158 . . . . . . . . . . . 12 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → z = ∅))
144 oveq1 5439 . . . . . . . . . . . . . 14 (z = ∅ → (z ·𝑜 𝑡) = (∅ ·𝑜 𝑡))
145144eqeq1d 2026 . . . . . . . . . . . . 13 (z = ∅ → ((z ·𝑜 𝑡) = ∅ ↔ (∅ ·𝑜 𝑡) = ∅))
14676, 145syl5ibrcom 146 . . . . . . . . . . . 12 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z = ∅ → (z ·𝑜 𝑡) = ∅))
147143, 146syld 40 . . . . . . . . . . 11 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (z ·𝑜 𝑡) = ∅))
148128, 147jcad 291 . . . . . . . . . 10 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → ((w ·𝑜 𝑠) = ∅ (z ·𝑜 𝑡) = ∅)))
149 eqtr3 2037 . . . . . . . . . . 11 (((w ·𝑜 𝑠) = ∅ (z ·𝑜 𝑡) = ∅) → (w ·𝑜 𝑠) = (z ·𝑜 𝑡))
150149eqcomd 2023 . . . . . . . . . 10 (((w ·𝑜 𝑠) = ∅ (z ·𝑜 𝑡) = ∅) → (z ·𝑜 𝑡) = (w ·𝑜 𝑠))
151148, 150syl6 29 . . . . . . . . 9 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ → (z ·𝑜 𝑡) = (w ·𝑜 𝑠)))
152 simplr 470 . . . . . . . . . . . . . . . . 17 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (z ·𝑜 u) = (w ·𝑜 v))
15391, 152oveq12d 5450 . . . . . . . . . . . . . . . 16 ((((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → ((v ·𝑜 𝑡) ·𝑜 (z ·𝑜 u)) = ((u ·𝑜 𝑠) ·𝑜 (w ·𝑜 v)))
154153adantl 262 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((v ·𝑜 𝑡) ·𝑜 (z ·𝑜 u)) = ((u ·𝑜 𝑠) ·𝑜 (w ·𝑜 v)))
155100simpld 105 . . . . . . . . . . . . . . . . 17 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → v 𝜔)
156 nnmcl 5971 . . . . . . . . . . . . . . . . 17 ((v 𝜔 𝑡 𝜔) → (v ·𝑜 𝑡) 𝜔)
157155, 74, 156syl2anc 393 . . . . . . . . . . . . . . . 16 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v ·𝑜 𝑡) 𝜔)
158 nnmcom 5979 . . . . . . . . . . . . . . . . 17 ((𝑐 𝜔 𝑑 𝜔) → (𝑐 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑐))
159158adantl 262 . . . . . . . . . . . . . . . 16 ((((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) (𝑐 𝜔 𝑑 𝜔)) → (𝑐 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑐))
160 nnmass 5977 . . . . . . . . . . . . . . . . 17 ((𝑐 𝜔 𝑑 𝜔 𝑒 𝜔) → ((𝑐 ·𝑜 𝑑) ·𝑜 𝑒) = (𝑐 ·𝑜 (𝑑 ·𝑜 𝑒)))
161160adantl 262 . . . . . . . . . . . . . . . 16 ((((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) (𝑐 𝜔 𝑑 𝜔 𝑒 𝜔)) → ((𝑐 ·𝑜 𝑑) ·𝑜 𝑒) = (𝑐 ·𝑜 (𝑑 ·𝑜 𝑒)))
162157, 135, 103, 159, 161caov13d 5603 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((v ·𝑜 𝑡) ·𝑜 (z ·𝑜 u)) = (u ·𝑜 (z ·𝑜 (v ·𝑜 𝑡))))
163 nnmcl 5971 . . . . . . . . . . . . . . . . 17 ((w 𝜔 v 𝜔) → (w ·𝑜 v) 𝜔)
164122, 155, 163syl2anc 393 . . . . . . . . . . . . . . . 16 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (w ·𝑜 v) 𝜔)
165161, 103, 104, 164caovassd 5579 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((u ·𝑜 𝑠) ·𝑜 (w ·𝑜 v)) = (u ·𝑜 (𝑠 ·𝑜 (w ·𝑜 v))))
166154, 162, 1653eqtr3d 2058 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (u ·𝑜 (z ·𝑜 (v ·𝑜 𝑡))) = (u ·𝑜 (𝑠 ·𝑜 (w ·𝑜 v))))
167 nnmcl 5971 . . . . . . . . . . . . . . . 16 ((z 𝜔 (v ·𝑜 𝑡) 𝜔) → (z ·𝑜 (v ·𝑜 𝑡)) 𝜔)
168135, 157, 167syl2anc 393 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z ·𝑜 (v ·𝑜 𝑡)) 𝜔)
169 nnmcl 5971 . . . . . . . . . . . . . . . 16 ((𝑠 𝜔 (w ·𝑜 v) 𝜔) → (𝑠 ·𝑜 (w ·𝑜 v)) 𝜔)
170104, 164, 169syl2anc 393 . . . . . . . . . . . . . . 15 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 ·𝑜 (w ·𝑜 v)) 𝜔)
171 nnmcan 5999 . . . . . . . . . . . . . . 15 (((u 𝜔 (z ·𝑜 (v ·𝑜 𝑡)) 𝜔 (𝑠 ·𝑜 (w ·𝑜 v)) 𝜔) u) → ((u ·𝑜 (z ·𝑜 (v ·𝑜 𝑡))) = (u ·𝑜 (𝑠 ·𝑜 (w ·𝑜 v))) ↔ (z ·𝑜 (v ·𝑜 𝑡)) = (𝑠 ·𝑜 (w ·𝑜 v))))
172103, 168, 170, 110, 171syl31anc 1122 . . . . . . . . . . . . . 14 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((u ·𝑜 (z ·𝑜 (v ·𝑜 𝑡))) = (u ·𝑜 (𝑠 ·𝑜 (w ·𝑜 v))) ↔ (z ·𝑜 (v ·𝑜 𝑡)) = (𝑠 ·𝑜 (w ·𝑜 v))))
173166, 172mpbid 135 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z ·𝑜 (v ·𝑜 𝑡)) = (𝑠 ·𝑜 (w ·𝑜 v)))
174135, 155, 74, 159, 161caov12d 5601 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z ·𝑜 (v ·𝑜 𝑡)) = (v ·𝑜 (z ·𝑜 𝑡)))
175104, 122, 155, 159, 161caov13d 5603 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 ·𝑜 (w ·𝑜 v)) = (v ·𝑜 (w ·𝑜 𝑠)))
176173, 174, 1753eqtr3d 2058 . . . . . . . . . . . 12 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v ·𝑜 (z ·𝑜 𝑡)) = (v ·𝑜 (w ·𝑜 𝑠)))
177176adantr 261 . . . . . . . . . . 11 ((((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) v) → (v ·𝑜 (z ·𝑜 𝑡)) = (v ·𝑜 (w ·𝑜 𝑠)))
178 nnmcl 5971 . . . . . . . . . . . . . 14 ((z 𝜔 𝑡 𝜔) → (z ·𝑜 𝑡) 𝜔)
179135, 74, 178syl2anc 393 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z ·𝑜 𝑡) 𝜔)
180 nnmcl 5971 . . . . . . . . . . . . . 14 ((w 𝜔 𝑠 𝜔) → (w ·𝑜 𝑠) 𝜔)
181122, 104, 180syl2anc 393 . . . . . . . . . . . . 13 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (w ·𝑜 𝑠) 𝜔)
182155, 179, 1813jca 1067 . . . . . . . . . . . 12 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v 𝜔 (z ·𝑜 𝑡) 𝜔 (w ·𝑜 𝑠) 𝜔))
183 nnmcan 5999 . . . . . . . . . . . 12 (((v 𝜔 (z ·𝑜 𝑡) 𝜔 (w ·𝑜 𝑠) 𝜔) v) → ((v ·𝑜 (z ·𝑜 𝑡)) = (v ·𝑜 (w ·𝑜 𝑠)) ↔ (z ·𝑜 𝑡) = (w ·𝑜 𝑠)))
184182, 183sylan 267 . . . . . . . . . . 11 ((((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) v) → ((v ·𝑜 (z ·𝑜 𝑡)) = (v ·𝑜 (w ·𝑜 𝑠)) ↔ (z ·𝑜 𝑡) = (w ·𝑜 𝑠)))
185177, 184mpbid 135 . . . . . . . . . 10 ((((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) v) → (z ·𝑜 𝑡) = (w ·𝑜 𝑠))
186185ex 108 . . . . . . . . 9 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (∅ v → (z ·𝑜 𝑡) = (w ·𝑜 𝑠)))
187 0elnn 4263 . . . . . . . . . 10 (v 𝜔 → (v = ∅ v))
188155, 187syl 14 . . . . . . . . 9 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (v = ∅ v))
189151, 186, 188mpjaod 625 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (z ·𝑜 𝑡) = (w ·𝑜 𝑠))
19061, 65, 189jca32 293 . . . . . . 7 (((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
1911902eximi 1470 . . . . . 6 (𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑠𝑡((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
192191exlimivv 1754 . . . . 5 (𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑠𝑡((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
193192exlimivv 1754 . . . 4 (vu𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑠𝑡((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
1941932eximi 1470 . . 3 (zwvu𝑎𝑏𝑠𝑡((f (𝜔 × N) g (𝜔 × N) (𝜔 × N)) (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ((g = ⟨𝑎, 𝑏 = ⟨𝑠, 𝑡⟩) (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → zw𝑠𝑡((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
19559, 194syl 14 . 2 ((f ~Q0 g g ~Q0 ) → zw𝑠𝑡((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
196 19.42vvvv 1768 . . 3 (zw𝑠𝑡((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))) ↔ ((f (𝜔 × N) (𝜔 × N)) zw𝑠𝑡((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
1975anbi1d 441 . . . . . . 7 (x = f → ((x = ⟨z, w y = ⟨𝑠, 𝑡⟩) ↔ (f = ⟨z, w y = ⟨𝑠, 𝑡⟩)))
198197anbi1d 441 . . . . . 6 (x = f → (((x = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠)) ↔ ((f = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
1991984exbidv 1728 . . . . 5 (x = f → (zw𝑠𝑡((x = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠)) ↔ zw𝑠𝑡((f = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
2004, 199anbi12d 445 . . . 4 (x = f → (((x (𝜔 × N) y (𝜔 × N)) zw𝑠𝑡((x = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))) ↔ ((f (𝜔 × N) y (𝜔 × N)) zw𝑠𝑡((f = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠)))))
20127anbi2d 440 . . . . 5 (y = → ((f (𝜔 × N) y (𝜔 × N)) ↔ (f (𝜔 × N) (𝜔 × N))))
20229anbi2d 440 . . . . . . 7 (y = → ((f = ⟨z, w y = ⟨𝑠, 𝑡⟩) ↔ (f = ⟨z, w = ⟨𝑠, 𝑡⟩)))
203202anbi1d 441 . . . . . 6 (y = → (((f = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠)) ↔ ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
2042034exbidv 1728 . . . . 5 (y = → (zw𝑠𝑡((f = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠)) ↔ zw𝑠𝑡((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
205201, 204anbi12d 445 . . . 4 (y = → (((f (𝜔 × N) y (𝜔 × N)) zw𝑠𝑡((f = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))) ↔ ((f (𝜔 × N) (𝜔 × N)) zw𝑠𝑡((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠)))))
206 df-enq0 6273 . . . 4 ~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zw𝑠𝑡((x = ⟨z, w y = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠)))}
2071, 19, 200, 205, 206brab 3979 . . 3 (f ~Q0 ↔ ((f (𝜔 × N) (𝜔 × N)) zw𝑠𝑡((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))))
208196, 207bitr4i 176 . 2 (zw𝑠𝑡((f (𝜔 × N) (𝜔 × N)) ((f = ⟨z, w = ⟨𝑠, 𝑡⟩) (z ·𝑜 𝑡) = (w ·𝑜 𝑠))) ↔ f ~Q0 )
209195, 208sylib 127 1 ((f ~Q0 g g ~Q0 ) → f ~Q0 )
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616   ∧ w3a 871   = wceq 1226  ∃wex 1358   ∈ wcel 1370  ∅c0 3197  ⟨cop 3349   class class class wbr 3734  𝜔com 4236   × cxp 4266  (class class class)co 5432   ·𝑜 comu 5910  Ncnpi 6126   ~Q0 ceq0 6140 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-coll 3842  ax-sep 3845  ax-nul 3853  ax-pow 3897  ax-pr 3914  ax-un 4116  ax-setind 4200  ax-iinf 4234 This theorem depends on definitions:  df-bi 110  df-dc 731  df-3or 872  df-3an 873  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ne 2184  df-ral 2285  df-rex 2286  df-reu 2287  df-rab 2289  df-v 2533  df-sbc 2738  df-csb 2826  df-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-int 3586  df-iun 3629  df-br 3735  df-opab 3789  df-mpt 3790  df-tr 3825  df-id 4000  df-iord 4048  df-on 4050  df-suc 4053  df-iom 4237  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-res 4280  df-ima 4281  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-fo 4831  df-f1o 4832  df-fv 4833  df-ov 5435  df-oprab 5436  df-mpt2 5437  df-1st 5686  df-2nd 5687  df-recs 5838  df-irdg 5874  df-oadd 5916  df-omul 5917  df-ni 6158  df-enq0 6273 This theorem is referenced by:  enq0er  6284
 Copyright terms: Public domain W3C validator