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

Theorem enq0sym 6414
Description: The equivalence relation for non-negative fractions is symmetric. Lemma for enq0er 6417. (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 2554 . . . . . . . 8 f V
2 vex 2554 . . . . . . . 8 g V
3 eleq1 2097 . . . . . . . . . 10 (x = f → (x (𝜔 × N) ↔ f (𝜔 × N)))
43anbi1d 438 . . . . . . . . 9 (x = f → ((x (𝜔 × N) y (𝜔 × N)) ↔ (f (𝜔 × N) y (𝜔 × N))))
5 eqeq1 2043 . . . . . . . . . . . 12 (x = f → (x = ⟨z, w⟩ ↔ f = ⟨z, w⟩))
65anbi1d 438 . . . . . . . . . . 11 (x = f → ((x = ⟨z, w y = ⟨v, u⟩) ↔ (f = ⟨z, w y = ⟨v, u⟩)))
76anbi1d 438 . . . . . . . . . 10 (x = f → (((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
874exbidv 1747 . . . . . . . . 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 442 . . . . . . . 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 2097 . . . . . . . . . 10 (y = g → (y (𝜔 × N) ↔ g (𝜔 × N)))
1110anbi2d 437 . . . . . . . . 9 (y = g → ((f (𝜔 × N) y (𝜔 × N)) ↔ (f (𝜔 × N) g (𝜔 × N))))
12 eqeq1 2043 . . . . . . . . . . . 12 (y = g → (y = ⟨v, u⟩ ↔ g = ⟨v, u⟩))
1312anbi2d 437 . . . . . . . . . . 11 (y = g → ((f = ⟨z, w y = ⟨v, u⟩) ↔ (f = ⟨z, w g = ⟨v, u⟩)))
1413anbi1d 438 . . . . . . . . . 10 (y = g → (((f = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
15144exbidv 1747 . . . . . . . . 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 442 . . . . . . . 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 6406 . . . . . . . 8 ~Q0 = {⟨x, y⟩ ∣ ((x (𝜔 × N) y (𝜔 × N)) zwvu((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)))}
181, 2, 9, 16, 17brab 4000 . . . . . . 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 3542 . . . . . . . . . . 11 ((z = 𝑎 w = 𝑏) → ⟨z, w⟩ = ⟨𝑎, 𝑏⟩)
2120eqeq2d 2048 . . . . . . . . . 10 ((z = 𝑎 w = 𝑏) → (f = ⟨z, w⟩ ↔ f = ⟨𝑎, 𝑏⟩))
2221anbi1d 438 . . . . . . . . 9 ((z = 𝑎 w = 𝑏) → ((f = ⟨z, w g = ⟨v, u⟩) ↔ (f = ⟨𝑎, 𝑏 g = ⟨v, u⟩)))
23 simpl 102 . . . . . . . . . . 11 ((z = 𝑎 w = 𝑏) → z = 𝑎)
2423oveq1d 5470 . . . . . . . . . 10 ((z = 𝑎 w = 𝑏) → (z ·𝑜 u) = (𝑎 ·𝑜 u))
25 simpr 103 . . . . . . . . . . 11 ((z = 𝑎 w = 𝑏) → w = 𝑏)
2625oveq1d 5470 . . . . . . . . . 10 ((z = 𝑎 w = 𝑏) → (w ·𝑜 v) = (𝑏 ·𝑜 v))
2724, 26eqeq12d 2051 . . . . . . . . 9 ((z = 𝑎 w = 𝑏) → ((z ·𝑜 u) = (w ·𝑜 v) ↔ (𝑎 ·𝑜 u) = (𝑏 ·𝑜 v)))
2822, 27anbi12d 442 . . . . . . . 8 ((z = 𝑎 w = 𝑏) → (((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((f = ⟨𝑎, 𝑏 g = ⟨v, u⟩) (𝑎 ·𝑜 u) = (𝑏 ·𝑜 v))))
29 opeq12 3542 . . . . . . . . . . 11 ((v = 𝑐 u = 𝑑) → ⟨v, u⟩ = ⟨𝑐, 𝑑⟩)
3029eqeq2d 2048 . . . . . . . . . 10 ((v = 𝑐 u = 𝑑) → (g = ⟨v, u⟩ ↔ g = ⟨𝑐, 𝑑⟩))
3130anbi2d 437 . . . . . . . . 9 ((v = 𝑐 u = 𝑑) → ((f = ⟨𝑎, 𝑏 g = ⟨v, u⟩) ↔ (f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩)))
32 simpr 103 . . . . . . . . . . 11 ((v = 𝑐 u = 𝑑) → u = 𝑑)
3332oveq2d 5471 . . . . . . . . . 10 ((v = 𝑐 u = 𝑑) → (𝑎 ·𝑜 u) = (𝑎 ·𝑜 𝑑))
34 simpl 102 . . . . . . . . . . 11 ((v = 𝑐 u = 𝑑) → v = 𝑐)
3534oveq2d 5471 . . . . . . . . . 10 ((v = 𝑐 u = 𝑑) → (𝑏 ·𝑜 v) = (𝑏 ·𝑜 𝑐))
3633, 35eqeq12d 2051 . . . . . . . . 9 ((v = 𝑐 u = 𝑑) → ((𝑎 ·𝑜 u) = (𝑏 ·𝑜 v) ↔ (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐)))
3731, 36anbi12d 442 . . . . . . . 8 ((v = 𝑐 u = 𝑑) → (((f = ⟨𝑎, 𝑏 g = ⟨v, u⟩) (𝑎 ·𝑜 u) = (𝑏 ·𝑜 v)) ↔ ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
3828, 37cbvex4v 1802 . . . . . . 7 (zwvu((f = ⟨z, w g = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ 𝑎𝑏𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐)))
3938anbi2i 430 . . . . . 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 1785 . . . . 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 1785 . . . . 5 (𝑐𝑑((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) ↔ ((f (𝜔 × N) g (𝜔 × N)) 𝑐𝑑((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))))
44432exbii 1494 . . . 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 459 . . . . . 6 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩))
50 simprr 484 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))
51 eleq1 2097 . . . . . . . . . . . . . 14 (f = ⟨𝑎, 𝑏⟩ → (f (𝜔 × N) ↔ ⟨𝑎, 𝑏 (𝜔 × N)))
52 opelxp 4317 . . . . . . . . . . . . . 14 (⟨𝑎, 𝑏 (𝜔 × N) ↔ (𝑎 𝜔 𝑏 N))
5351, 52syl6bb 185 . . . . . . . . . . . . 13 (f = ⟨𝑎, 𝑏⟩ → (f (𝜔 × N) ↔ (𝑎 𝜔 𝑏 N)))
5453biimpcd 148 . . . . . . . . . . . 12 (f (𝜔 × N) → (f = ⟨𝑎, 𝑏⟩ → (𝑎 𝜔 𝑏 N)))
55 eleq1 2097 . . . . . . . . . . . . . 14 (g = ⟨𝑐, 𝑑⟩ → (g (𝜔 × N) ↔ ⟨𝑐, 𝑑 (𝜔 × N)))
56 opelxp 4317 . . . . . . . . . . . . . 14 (⟨𝑐, 𝑑 (𝜔 × N) ↔ (𝑐 𝜔 𝑑 N))
5755, 56syl6bb 185 . . . . . . . . . . . . 13 (g = ⟨𝑐, 𝑑⟩ → (g (𝜔 × N) ↔ (𝑐 𝜔 𝑑 N)))
5857biimpcd 148 . . . . . . . . . . . 12 (g (𝜔 × N) → (g = ⟨𝑐, 𝑑⟩ → (𝑐 𝜔 𝑑 N)))
5954, 58im2anan9 530 . . . . . . . . . . 11 ((f (𝜔 × N) g (𝜔 × N)) → ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) → ((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N))))
6059imp 115 . . . . . . . . . 10 (((f (𝜔 × N) g (𝜔 × N)) (f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩)) → ((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N)))
6160adantrr 448 . . . . . . . . 9 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → ((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N)))
62 pinn 6293 . . . . . . . . . . . 12 (𝑑 N𝑑 𝜔)
63 nnmcom 6007 . . . . . . . . . . . 12 ((𝑎 𝜔 𝑑 𝜔) → (𝑎 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑎))
6462, 63sylan2 270 . . . . . . . . . . 11 ((𝑎 𝜔 𝑑 N) → (𝑎 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑎))
65 pinn 6293 . . . . . . . . . . . 12 (𝑏 N𝑏 𝜔)
66 nnmcom 6007 . . . . . . . . . . . 12 ((𝑏 𝜔 𝑐 𝜔) → (𝑏 ·𝑜 𝑐) = (𝑐 ·𝑜 𝑏))
6765, 66sylan 267 . . . . . . . . . . 11 ((𝑏 N 𝑐 𝜔) → (𝑏 ·𝑜 𝑐) = (𝑐 ·𝑜 𝑏))
6864, 67eqeqan12d 2052 . . . . . . . . . 10 (((𝑎 𝜔 𝑑 N) (𝑏 N 𝑐 𝜔)) → ((𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐) ↔ (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏)))
6968an42s 523 . . . . . . . . 9 (((𝑎 𝜔 𝑏 N) (𝑐 𝜔 𝑑 N)) → ((𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐) ↔ (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏)))
7061, 69syl 14 . . . . . . . 8 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → ((𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐) ↔ (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏)))
7150, 70mpbid 135 . . . . . . 7 (((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → (𝑑 ·𝑜 𝑎) = (𝑐 ·𝑜 𝑏))
7271eqcomd 2042 . . . . . 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 1489 . . . 4 (𝑐𝑑((f (𝜔 × N) g (𝜔 × N)) ((f = ⟨𝑎, 𝑏 g = ⟨𝑐, 𝑑⟩) (𝑎 ·𝑜 𝑑) = (𝑏 ·𝑜 𝑐))) → 𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
75742eximi 1489 . . 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 1578 . . 3 (𝑎𝑏𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ 𝑐𝑑𝑎𝑏((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
78 19.42vv 1785 . . . . 5 (𝑎𝑏((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ ((g (𝜔 × N) f (𝜔 × N)) 𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
79782exbii 1494 . . . 4 (𝑐𝑑𝑎𝑏((g (𝜔 × N) f (𝜔 × N)) ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ 𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) 𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
80 19.42vv 1785 . . . . 5 (𝑐𝑑((g (𝜔 × N) f (𝜔 × N)) 𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))) ↔ ((g (𝜔 × N) f (𝜔 × N)) 𝑐𝑑𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
81 opeq12 3542 . . . . . . . . . 10 ((z = 𝑐 w = 𝑑) → ⟨z, w⟩ = ⟨𝑐, 𝑑⟩)
8281eqeq2d 2048 . . . . . . . . 9 ((z = 𝑐 w = 𝑑) → (g = ⟨z, w⟩ ↔ g = ⟨𝑐, 𝑑⟩))
8382anbi1d 438 . . . . . . . 8 ((z = 𝑐 w = 𝑑) → ((g = ⟨z, w f = ⟨v, u⟩) ↔ (g = ⟨𝑐, 𝑑 f = ⟨v, u⟩)))
84 simpl 102 . . . . . . . . . 10 ((z = 𝑐 w = 𝑑) → z = 𝑐)
8584oveq1d 5470 . . . . . . . . 9 ((z = 𝑐 w = 𝑑) → (z ·𝑜 u) = (𝑐 ·𝑜 u))
86 simpr 103 . . . . . . . . . 10 ((z = 𝑐 w = 𝑑) → w = 𝑑)
8786oveq1d 5470 . . . . . . . . 9 ((z = 𝑐 w = 𝑑) → (w ·𝑜 v) = (𝑑 ·𝑜 v))
8885, 87eqeq12d 2051 . . . . . . . 8 ((z = 𝑐 w = 𝑑) → ((z ·𝑜 u) = (w ·𝑜 v) ↔ (𝑐 ·𝑜 u) = (𝑑 ·𝑜 v)))
8983, 88anbi12d 442 . . . . . . 7 ((z = 𝑐 w = 𝑑) → (((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((g = ⟨𝑐, 𝑑 f = ⟨v, u⟩) (𝑐 ·𝑜 u) = (𝑑 ·𝑜 v))))
90 opeq12 3542 . . . . . . . . . 10 ((v = 𝑎 u = 𝑏) → ⟨v, u⟩ = ⟨𝑎, 𝑏⟩)
9190eqeq2d 2048 . . . . . . . . 9 ((v = 𝑎 u = 𝑏) → (f = ⟨v, u⟩ ↔ f = ⟨𝑎, 𝑏⟩))
9291anbi2d 437 . . . . . . . 8 ((v = 𝑎 u = 𝑏) → ((g = ⟨𝑐, 𝑑 f = ⟨v, u⟩) ↔ (g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩)))
93 simpr 103 . . . . . . . . . 10 ((v = 𝑎 u = 𝑏) → u = 𝑏)
9493oveq2d 5471 . . . . . . . . 9 ((v = 𝑎 u = 𝑏) → (𝑐 ·𝑜 u) = (𝑐 ·𝑜 𝑏))
95 simpl 102 . . . . . . . . . 10 ((v = 𝑎 u = 𝑏) → v = 𝑎)
9695oveq2d 5471 . . . . . . . . 9 ((v = 𝑎 u = 𝑏) → (𝑑 ·𝑜 v) = (𝑑 ·𝑜 𝑎))
9794, 96eqeq12d 2051 . . . . . . . 8 ((v = 𝑎 u = 𝑏) → ((𝑐 ·𝑜 u) = (𝑑 ·𝑜 v) ↔ (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎)))
9892, 97anbi12d 442 . . . . . . 7 ((v = 𝑎 u = 𝑏) → (((g = ⟨𝑐, 𝑑 f = ⟨v, u⟩) (𝑐 ·𝑜 u) = (𝑑 ·𝑜 v)) ↔ ((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎))))
9989, 98cbvex4v 1802 . . . . . 6 (zwvu((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ 𝑐𝑑𝑎𝑏((g = ⟨𝑐, 𝑑 f = ⟨𝑎, 𝑏⟩) (𝑐 ·𝑜 𝑏) = (𝑑 ·𝑜 𝑎)))
100 eleq1 2097 . . . . . . . . . 10 (x = g → (x (𝜔 × N) ↔ g (𝜔 × N)))
101100anbi1d 438 . . . . . . . . 9 (x = g → ((x (𝜔 × N) y (𝜔 × N)) ↔ (g (𝜔 × N) y (𝜔 × N))))
102 eqeq1 2043 . . . . . . . . . . . 12 (x = g → (x = ⟨z, w⟩ ↔ g = ⟨z, w⟩))
103102anbi1d 438 . . . . . . . . . . 11 (x = g → ((x = ⟨z, w y = ⟨v, u⟩) ↔ (g = ⟨z, w y = ⟨v, u⟩)))
104103anbi1d 438 . . . . . . . . . 10 (x = g → (((x = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
1051044exbidv 1747 . . . . . . . . 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 442 . . . . . . . 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 2097 . . . . . . . . . 10 (y = f → (y (𝜔 × N) ↔ f (𝜔 × N)))
108107anbi2d 437 . . . . . . . . 9 (y = f → ((g (𝜔 × N) y (𝜔 × N)) ↔ (g (𝜔 × N) f (𝜔 × N))))
109 eqeq1 2043 . . . . . . . . . . . 12 (y = f → (y = ⟨v, u⟩ ↔ f = ⟨v, u⟩))
110109anbi2d 437 . . . . . . . . . . 11 (y = f → ((g = ⟨z, w y = ⟨v, u⟩) ↔ (g = ⟨z, w f = ⟨v, u⟩)))
111110anbi1d 438 . . . . . . . . . 10 (y = f → (((g = ⟨z, w y = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v)) ↔ ((g = ⟨z, w f = ⟨v, u⟩) (z ·𝑜 u) = (w ·𝑜 v))))
1121114exbidv 1747 . . . . . . . . 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 442 . . . . . . . 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 4000 . . . . . . 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 1242  wex 1378   wcel 1390  cop 3370   class class class wbr 3755  𝜔com 4256   × cxp 4286  (class class class)co 5455   ·𝑜 comu 5938  Ncnpi 6256   ~Q0 ceq0 6270
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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-coll 3863  ax-sep 3866  ax-nul 3874  ax-pow 3918  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-iinf 4254
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-iun 3650  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  df-iom 4257  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460  df-1st 5709  df-2nd 5710  df-recs 5861  df-irdg 5897  df-oadd 5944  df-omul 5945  df-ni 6288  df-enq0 6406
This theorem is referenced by:  enq0er  6417
  Copyright terms: Public domain W3C validator