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

Theorem enq0sym 6281
Description: The equivalence relation for non-negative fractions is symmetric. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.)
Assertion
Ref Expression
enq0sym (f ~Q0 gg ~Q0 f)

Proof of Theorem enq0sym
Dummy variables 𝑎 𝑏 𝑐 𝑑 u v w x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2534 . . . . . . . 8 f V
2 vex 2534 . . . . . . . 8 g V
3 eleq1 2078 . . . . . . . . . 10 (x = f → (x (𝜔 × N) ↔ f (𝜔 × N)))
43anbi1d 441 . . . . . . . . 9 (x = f → ((x (𝜔 × N) y (𝜔 × N)) ↔ (f (𝜔 × N) y (𝜔 × N))))
5 eqeq1 2024 . . . . . . . . . . . 12 (x = f → (x = ⟨z, w⟩ ↔ f = ⟨z, w⟩))
65anbi1d 441 . . . . . . . . . . 11 (x = f → ((x = ⟨z, w y = ⟨v, u⟩) ↔ (f = ⟨z, w y = ⟨v, u⟩)))
76anbi1d 441 . . . . . . . . . 10 (x = f → (((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
874exbidv 1728 . . . . . . . . 9 (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 . . . . . . . 8 (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 . . . . . . . . . 10 (y = g → (y (𝜔 × N) ↔ g (𝜔 × N)))
1110anbi2d 440 . . . . . . . . 9 (y = g → ((f (𝜔 × N) y (𝜔 × N)) ↔ (f (𝜔 × N) g (𝜔 × N))))
12 eqeq1 2024 . . . . . . . . . . . 12 (y = g → (y = ⟨v, u⟩ ↔ g = ⟨v, u⟩))
1312anbi2d 440 . . . . . . . . . . 11 (y = g → ((f = ⟨z, w y = ⟨v, u⟩) ↔ (f = ⟨z, w g = ⟨v, u⟩)))
1413anbi1d 441 . . . . . . . . . 10 (y = g → (((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
15144exbidv 1728 . . . . . . . . 9 (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 . . . . . . . 8 (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 . . . . . . . 8 ~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))}
181, 2, 9, 16, 17brab 3979 . . . . . . 7 (f ~Q0 g ↔ ((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
1918biimpi 113 . . . . . 6 (f ~Q0 g → ((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
20 opeq12 3521 . . . . . . . . . . 11 ((z = 𝑎 w = 𝑏) → ⟨z, w⟩ = ⟨𝑎, 𝑏⟩)
2120eqeq2d 2029 . . . . . . . . . 10 ((z = 𝑎 w = 𝑏) → (f = ⟨z, w⟩ ↔ f = ⟨𝑎, 𝑏⟩))
2221anbi1d 441 . . . . . . . . 9 ((z = 𝑎 w = 𝑏) → ((f = ⟨z, w g = ⟨v, u⟩) ↔ (f = ⟨𝑎, 𝑏 g = ⟨v, u⟩)))
23 ax-ia1 99 . . . . . . . . . . 11 ((z = 𝑎 w = 𝑏) → z = 𝑎)
2423oveq1d 5447 . . . . . . . . . 10 ((z = 𝑎 w = 𝑏) → (z ·𝑜 u) = (𝑎 ·𝑜 u))
25 ax-ia2 100 . . . . . . . . . . 11 ((z = 𝑎 w = 𝑏) → w = 𝑏)
2625oveq1d 5447 . . . . . . . . . 10 ((z = 𝑎 w = 𝑏) → (w ·𝑜 v) = (𝑏 ·𝑜 v))
2724, 26eqeq12d 2032 . . . . . . . . 9 ((z = 𝑎 w = 𝑏) → ((z ·𝑜 u) = (w ·𝑜 v) ↔ (𝑎 ·𝑜 u) = (𝑏 ·𝑜 v)))
2822, 27anbi12d 445 . . . . . . . 8 ((z = 𝑎 w = 𝑏) → (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨𝑎, 𝑏 g = ⟨v, u⟩) (𝑎 ·𝑜 u) = (𝑏 ·𝑜 v))))
29 opeq12 3521 . . . . . . . . . . 11 ((v = 𝑐 u = 𝑑) → ⟨v, u⟩ = ⟨𝑐, 𝑑⟩)
3029eqeq2d 2029 . . . . . . . . . 10 ((v = 𝑐 u = 𝑑) → (g = ⟨v, u⟩ ↔ g = ⟨𝑐, 𝑑⟩))
3130anbi2d 440 . . . . . . . . 9 ((v = 𝑐 u = 𝑑) → ((f = ⟨𝑎, 𝑏 g = ⟨v, u⟩) ↔ (f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩)))
32 ax-ia2 100 . . . . . . . . . . 11 ((v = 𝑐 u = 𝑑) → u = 𝑑)
3332oveq2d 5448 . . . . . . . . . 10 ((v = 𝑐 u = 𝑑) → (𝑎 ·𝑜 u) = (𝑎 ·𝑜 𝑑))
34 ax-ia1 99 . . . . . . . . . . 11 ((v = 𝑐 u = 𝑑) → v = 𝑐)
3534oveq2d 5448 . . . . . . . . . 10 ((v = 𝑐 u = 𝑑) → (𝑏 ·𝑜 v) = (𝑏 ·𝑜 𝑐))
3633, 35eqeq12d 2032 . . . . . . . . 9 ((v = 𝑐 u = 𝑑) → ((𝑎 ·𝑜 u) = (𝑏 ·𝑜 v) ↔ (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐)))
3731, 36anbi12d 445 . . . . . . . 8 ((v = 𝑐 u = 𝑑) → (((f = ⟨𝑎, 𝑏 g = ⟨v, u⟩) (𝑎 ·𝑜 u) = (𝑏 ·𝑜 v)) ↔ ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
3828, 37cbvex4v 1783 . . . . . . 7 (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ 𝑎𝑏𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐)))
3938anbi2i 433 . . . . . 6 (((f (𝜔 × N) g (𝜔 × N)) zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((f (𝜔 × N) g (𝜔 × N)) 𝑎𝑏𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
4019, 39sylib 127 . . . . 5 (f ~Q0 g → ((f (𝜔 × N) g (𝜔 × N)) 𝑎𝑏𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
41 19.42vv 1766 . . . . 5 (𝑎𝑏((f (𝜔 × N) g (𝜔 × N)) 𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) ↔ ((f (𝜔 × N) g (𝜔 × N)) 𝑎𝑏𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
4240, 41sylibr 137 . . . 4 (f ~Q0 g𝑎𝑏((f (𝜔 × N) g (𝜔 × N)) 𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
43 19.42vv 1766 . . . . 5 (𝑐𝑑((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) ↔ ((f (𝜔 × N) g (𝜔 × N)) 𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
44432exbii 1475 . . . 4 (𝑎𝑏𝑐𝑑((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) ↔ 𝑎𝑏((f (𝜔 × N) g (𝜔 × N)) 𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
4542, 44sylibr 137 . . 3 (f ~Q0 g𝑎𝑏𝑐𝑑((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
46 pm3.22 252 . . . . . . 7 ((f (𝜔 × N) g (𝜔 × N)) → (g (𝜔 × N) f (𝜔 × N)))
4746adantr 261 . . . . . 6 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (g (𝜔 × N) f (𝜔 × N)))
48 pm3.22 252 . . . . . . 7 ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) → (g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩))
4948ad2antrl 463 . . . . . 6 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩))
50 simprr 472 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))
51 eleq1 2078 . . . . . . . . . . . . . 14 (f = ⟨𝑎, 𝑏⟩ → (f (𝜔 × N) ↔ ⟨𝑎, 𝑏 (𝜔 × N)))
52 opelxp 4297 . . . . . . . . . . . . . 14 (⟨𝑎, 𝑏 (𝜔 × N) ↔ (𝑎 𝜔 𝑏 N))
5351, 52syl6bb 185 . . . . . . . . . . . . 13 (f = ⟨𝑎, 𝑏⟩ → (f (𝜔 × N) ↔ (𝑎 𝜔 𝑏 N)))
5453biimpcd 148 . . . . . . . . . . . 12 (f (𝜔 × N) → (f = ⟨𝑎, 𝑏⟩ → (𝑎 𝜔 𝑏 N)))
55 eleq1 2078 . . . . . . . . . . . . . 14 (g = ⟨𝑐, 𝑑⟩ → (g (𝜔 × N) ↔ ⟨𝑐, 𝑑 (𝜔 × N)))
56 opelxp 4297 . . . . . . . . . . . . . 14 (⟨𝑐, 𝑑 (𝜔 × N) ↔ (𝑐 𝜔 𝑑 N))
5755, 56syl6bb 185 . . . . . . . . . . . . 13 (g = ⟨𝑐, 𝑑⟩ → (g (𝜔 × N) ↔ (𝑐 𝜔 𝑑 N)))
5857biimpcd 148 . . . . . . . . . . . 12 (g (𝜔 × N) → (g = ⟨𝑐, 𝑑⟩ → (𝑐 𝜔 𝑑 N)))
5954, 58im2anan9 517 . . . . . . . . . . 11 ((f (𝜔 × N) g (𝜔 × N)) → ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) → ((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N))))
6059imp 115 . . . . . . . . . 10 (((f (𝜔 × N) g (𝜔 × N)) (f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩)) → ((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N)))
6160adantrr 451 . . . . . . . . 9 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → ((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N)))
62 pinn 6163 . . . . . . . . . . . 12 (𝑑 N𝑑 𝜔)
63 nnmcom 5979 . . . . . . . . . . . 12 ((𝑎 𝜔 𝑑 𝜔) → (𝑎 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑎))
6462, 63sylan2 270 . . . . . . . . . . 11 ((𝑎 𝜔 𝑑 N) → (𝑎 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑎))
65 pinn 6163 . . . . . . . . . . . 12 (𝑏 N𝑏 𝜔)
66 nnmcom 5979 . . . . . . . . . . . 12 ((𝑏 𝜔 𝑐 𝜔) → (𝑏 ·𝑜 𝑐) = (𝑐 ·𝑜 𝑏))
6765, 66sylan 267 . . . . . . . . . . 11 ((𝑏 N 𝑐 𝜔) → (𝑏 ·𝑜 𝑐) = (𝑐 ·𝑜 𝑏))
6864, 67eqeqan12d 2033 . . . . . . . . . 10 (((𝑎 𝜔 𝑑 N) (𝑏 N 𝑐 𝜔)) → ((𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐) ↔ (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏)))
6968an42s 510 . . . . . . . . 9 (((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N)) → ((𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐) ↔ (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏)))
7061, 69syl 14 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → ((𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐) ↔ (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏)))
7150, 70mpbid 135 . . . . . . 7 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏))
7271eqcomd 2023 . . . . . 6 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))
7347, 49, 72jca32 293 . . . . 5 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → ((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
74732eximi 1470 . . . 4 (𝑐𝑑((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → 𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
75742eximi 1470 . . 3 (𝑎𝑏𝑐𝑑((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → 𝑎𝑏𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
7645, 75syl 14 . 2 (f ~Q0 g𝑎𝑏𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
77 exrot4 1559 . . 3 (𝑎𝑏𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ 𝑐𝑑𝑎𝑏((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
78 19.42vv 1766 . . . . 5 (𝑎𝑏((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ ((g (𝜔 × N) f (𝜔 × N)) 𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
79782exbii 1475 . . . 4 (𝑐𝑑𝑎𝑏((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ 𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) 𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
80 19.42vv 1766 . . . . 5 (𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) 𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ ((g (𝜔 × N) f (𝜔 × N)) 𝑐𝑑𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
81 opeq12 3521 . . . . . . . . . 10 ((z = 𝑐 w = 𝑑) → ⟨z, w⟩ = ⟨𝑐, 𝑑⟩)
8281eqeq2d 2029 . . . . . . . . 9 ((z = 𝑐 w = 𝑑) → (g = ⟨z, w⟩ ↔ g = ⟨𝑐, 𝑑⟩))
8382anbi1d 441 . . . . . . . 8 ((z = 𝑐 w = 𝑑) → ((g = ⟨z, w f = ⟨v, u⟩) ↔ (g = ⟨𝑐, 𝑑 f = ⟨v, u⟩)))
84 ax-ia1 99 . . . . . . . . . 10 ((z = 𝑐 w = 𝑑) → z = 𝑐)
8584oveq1d 5447 . . . . . . . . 9 ((z = 𝑐 w = 𝑑) → (z ·𝑜 u) = (𝑐 ·𝑜 u))
86 ax-ia2 100 . . . . . . . . . 10 ((z = 𝑐 w = 𝑑) → w = 𝑑)
8786oveq1d 5447 . . . . . . . . 9 ((z = 𝑐 w = 𝑑) → (w ·𝑜 v) = (𝑑 ·𝑜 v))
8885, 87eqeq12d 2032 . . . . . . . 8 ((z = 𝑐 w = 𝑑) → ((z ·𝑜 u) = (w ·𝑜 v) ↔ (𝑐 ·𝑜 u) = (𝑑 ·𝑜 v)))
8983, 88anbi12d 445 . . . . . . 7 ((z = 𝑐 w = 𝑑) → (((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((g = ⟨𝑐, 𝑑 f = ⟨v, u⟩) (𝑐 ·𝑜 u) = (𝑑 ·𝑜 v))))
90 opeq12 3521 . . . . . . . . . 10 ((v = 𝑎 u = 𝑏) → ⟨v, u⟩ = ⟨𝑎, 𝑏⟩)
9190eqeq2d 2029 . . . . . . . . 9 ((v = 𝑎 u = 𝑏) → (f = ⟨v, u⟩ ↔ f = ⟨𝑎, 𝑏⟩))
9291anbi2d 440 . . . . . . . 8 ((v = 𝑎 u = 𝑏) → ((g = ⟨𝑐, 𝑑 f = ⟨v, u⟩) ↔ (g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩)))
93 ax-ia2 100 . . . . . . . . . 10 ((v = 𝑎 u = 𝑏) → u = 𝑏)
9493oveq2d 5448 . . . . . . . . 9 ((v = 𝑎 u = 𝑏) → (𝑐 ·𝑜 u) = (𝑐 ·𝑜 𝑏))
95 ax-ia1 99 . . . . . . . . . 10 ((v = 𝑎 u = 𝑏) → v = 𝑎)
9695oveq2d 5448 . . . . . . . . 9 ((v = 𝑎 u = 𝑏) → (𝑑 ·𝑜 v) = (𝑑 ·𝑜 𝑎))
9794, 96eqeq12d 2032 . . . . . . . 8 ((v = 𝑎 u = 𝑏) → ((𝑐 ·𝑜 u) = (𝑑 ·𝑜 v) ↔ (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎)))
9892, 97anbi12d 445 . . . . . . 7 ((v = 𝑎 u = 𝑏) → (((g = ⟨𝑐, 𝑑 f = ⟨v, u⟩) (𝑐 ·𝑜 u) = (𝑑 ·𝑜 v)) ↔ ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
9989, 98cbvex4v 1783 . . . . . 6 (zwvu((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ 𝑐𝑑𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎)))
100 eleq1 2078 . . . . . . . . . 10 (x = g → (x (𝜔 × N) ↔ g (𝜔 × N)))
101100anbi1d 441 . . . . . . . . 9 (x = g → ((x (𝜔 × N) y (𝜔 × N)) ↔ (g (𝜔 × N) y (𝜔 × N))))
102 eqeq1 2024 . . . . . . . . . . . 12 (x = g → (x = ⟨z, w⟩ ↔ g = ⟨z, w⟩))
103102anbi1d 441 . . . . . . . . . . 11 (x = g → ((x = ⟨z, w y = ⟨v, u⟩) ↔ (g = ⟨z, w y = ⟨v, u⟩)))
104103anbi1d 441 . . . . . . . . . 10 (x = g → (((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
1051044exbidv 1728 . . . . . . . . 9 (x = g → (zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ zwvu((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
106101, 105anbi12d 445 . . . . . . . 8 (x = g → (((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((g (𝜔 × N) y (𝜔 × N)) zwvu((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))))
107 eleq1 2078 . . . . . . . . . 10 (y = f → (y (𝜔 × N) ↔ f (𝜔 × N)))
108107anbi2d 440 . . . . . . . . 9 (y = f → ((g (𝜔 × N) y (𝜔 × N)) ↔ (g (𝜔 × N) f (𝜔 × N))))
109 eqeq1 2024 . . . . . . . . . . . 12 (y = f → (y = ⟨v, u⟩ ↔ f = ⟨v, u⟩))
110109anbi2d 440 . . . . . . . . . . 11 (y = f → ((g = ⟨z, w y = ⟨v, u⟩) ↔ (g = ⟨z, w f = ⟨v, u⟩)))
111110anbi1d 441 . . . . . . . . . 10 (y = f → (((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
1121114exbidv 1728 . . . . . . . . 9 (y = f → (zwvu((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ zwvu((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
113108, 112anbi12d 445 . . . . . . . 8 (y = f → (((g (𝜔 × N) y (𝜔 × N)) zwvu((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) ↔ ((g (𝜔 × N) f (𝜔 × N)) zwvu((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))))
1142, 1, 106, 113, 17brab 3979 . . . . . . 7 (g ~Q0 f ↔ ((g (𝜔 × N) f (𝜔 × N)) zwvu((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
115114biimpri 124 . . . . . 6 (((g (𝜔 × N) f (𝜔 × N)) zwvu((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))) → g ~Q0 f)
11699, 115sylan2br 272 . . . . 5 (((g (𝜔 × N) f (𝜔 × N)) 𝑐𝑑𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) → g ~Q0 f)
11780, 116sylbi 114 . . . 4 (𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) 𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) → g ~Q0 f)
11879, 117sylbi 114 . . 3 (𝑐𝑑𝑎𝑏((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) → g ~Q0 f)
11977, 118sylbi 114 . 2 (𝑎𝑏𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) → g ~Q0 f)
12076, 119syl 14 1 (f ~Q0 gg ~Q0 f)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1226  wex 1358   wcel 1370  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-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