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

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

Proof of Theorem enq0tr
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑠 𝑡 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2577 . . . . . . . . . 10 𝑓 ∈ V
2 vex 2577 . . . . . . . . . 10 𝑔 ∈ V
3 eleq1 2116 . . . . . . . . . . . 12 (𝑥 = 𝑓 → (𝑥 ∈ (ω × N) ↔ 𝑓 ∈ (ω × N)))
43anbi1d 446 . . . . . . . . . . 11 (𝑥 = 𝑓 → ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ↔ (𝑓 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N))))
5 eqeq1 2062 . . . . . . . . . . . . . 14 (𝑥 = 𝑓 → (𝑥 = ⟨𝑧, 𝑤⟩ ↔ 𝑓 = ⟨𝑧, 𝑤⟩))
65anbi1d 446 . . . . . . . . . . . . 13 (𝑥 = 𝑓 → ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ↔ (𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)))
76anbi1d 446 . . . . . . . . . . . 12 (𝑥 = 𝑓 → (((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ↔ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))))
874exbidv 1766 . . . . . . . . . . 11 (𝑥 = 𝑓 → (∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ↔ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))))
94, 8anbi12d 450 . . . . . . . . . 10 (𝑥 = 𝑓 → (((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))))
10 eleq1 2116 . . . . . . . . . . . 12 (𝑦 = 𝑔 → (𝑦 ∈ (ω × N) ↔ 𝑔 ∈ (ω × N)))
1110anbi2d 445 . . . . . . . . . . 11 (𝑦 = 𝑔 → ((𝑓 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ↔ (𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N))))
12 eqeq1 2062 . . . . . . . . . . . . . 14 (𝑦 = 𝑔 → (𝑦 = ⟨𝑣, 𝑢⟩ ↔ 𝑔 = ⟨𝑣, 𝑢⟩))
1312anbi2d 445 . . . . . . . . . . . . 13 (𝑦 = 𝑔 → ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ↔ (𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩)))
1413anbi1d 446 . . . . . . . . . . . 12 (𝑦 = 𝑔 → (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ↔ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))))
15144exbidv 1766 . . . . . . . . . . 11 (𝑦 = 𝑔 → (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ↔ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))))
1611, 15anbi12d 450 . . . . . . . . . 10 (𝑦 = 𝑔 → (((𝑓 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))))
17 df-enq0 6579 . . . . . . . . . 10 ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)))}
181, 2, 9, 16, 17brab 4036 . . . . . . . . 9 (𝑓 ~Q0 𝑔 ↔ ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))))
19 vex 2577 . . . . . . . . . 10 ∈ V
20 eleq1 2116 . . . . . . . . . . . 12 (𝑥 = 𝑔 → (𝑥 ∈ (ω × N) ↔ 𝑔 ∈ (ω × N)))
2120anbi1d 446 . . . . . . . . . . 11 (𝑥 = 𝑔 → ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ↔ (𝑔 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N))))
22 eqeq1 2062 . . . . . . . . . . . . . 14 (𝑥 = 𝑔 → (𝑥 = ⟨𝑎, 𝑏⟩ ↔ 𝑔 = ⟨𝑎, 𝑏⟩))
2322anbi1d 446 . . . . . . . . . . . . 13 (𝑥 = 𝑔 → ((𝑥 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ↔ (𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩)))
2423anbi1d 446 . . . . . . . . . . . 12 (𝑥 = 𝑔 → (((𝑥 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
25244exbidv 1766 . . . . . . . . . . 11 (𝑥 = 𝑔 → (∃𝑎𝑏𝑠𝑡((𝑥 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
2621, 25anbi12d 450 . . . . . . . . . 10 (𝑥 = 𝑔 → (((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑥 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) ↔ ((𝑔 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
27 eleq1 2116 . . . . . . . . . . . 12 (𝑦 = → (𝑦 ∈ (ω × N) ↔ ∈ (ω × N)))
2827anbi2d 445 . . . . . . . . . . 11 (𝑦 = → ((𝑔 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ↔ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))))
29 eqeq1 2062 . . . . . . . . . . . . . 14 (𝑦 = → (𝑦 = ⟨𝑠, 𝑡⟩ ↔ = ⟨𝑠, 𝑡⟩))
3029anbi2d 445 . . . . . . . . . . . . 13 (𝑦 = → ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ↔ (𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩)))
3130anbi1d 446 . . . . . . . . . . . 12 (𝑦 = → (((𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
32314exbidv 1766 . . . . . . . . . . 11 (𝑦 = → (∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)) ↔ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
3328, 32anbi12d 450 . . . . . . . . . 10 (𝑦 = → (((𝑔 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) ↔ ((𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
34 df-enq0 6579 . . . . . . . . . 10 ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑥 = ⟨𝑎, 𝑏⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))}
352, 19, 26, 33, 34brab 4036 . . . . . . . . 9 (𝑔 ~Q0 ↔ ((𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
3618, 35anbi12i 441 . . . . . . . 8 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) ↔ (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))) ∧ ((𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
3736biimpi 117 . . . . . . 7 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) → (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))) ∧ ((𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
38 an4 528 . . . . . . 7 ((((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))) ∧ ((𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))) ∧ (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
3937, 38sylib 131 . . . . . 6 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) → (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))) ∧ (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
40 3anass 900 . . . . . . . 8 ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ↔ (𝑓 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))))
41 anass 387 . . . . . . . . 9 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))) ↔ (𝑓 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N)))))
42 anass 387 . . . . . . . . . 10 (((𝑔 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∈ (ω × N)) ↔ (𝑔 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))))
4342anbi2i 438 . . . . . . . . 9 ((𝑓 ∈ (ω × N) ∧ ((𝑔 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∈ (ω × N))) ↔ (𝑓 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N)))))
44 anidm 382 . . . . . . . . . . 11 ((𝑔 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ↔ 𝑔 ∈ (ω × N))
4544anbi1i 439 . . . . . . . . . 10 (((𝑔 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∈ (ω × N)) ↔ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N)))
4645anbi2i 438 . . . . . . . . 9 ((𝑓 ∈ (ω × N) ∧ ((𝑔 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ ∈ (ω × N))) ↔ (𝑓 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))))
4741, 43, 463bitr2i 201 . . . . . . . 8 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))) ↔ (𝑓 ∈ (ω × N) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))))
4840, 47bitr4i 180 . . . . . . 7 ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))))
4948anbi1i 439 . . . . . 6 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N)) ∧ (𝑔 ∈ (ω × N) ∧ ∈ (ω × N))) ∧ (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5039, 49sylibr 141 . . . . 5 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) → ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
51 ee8anv 1826 . . . . . 6 (∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) ↔ (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))))
5251anbi2i 438 . . . . 5 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (∃𝑧𝑤𝑣𝑢((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ∃𝑎𝑏𝑠𝑡((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5350, 52sylibr 141 . . . 4 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) → ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
54 19.42vvvv 1806 . . . . . . 7 (∃𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
55542exbii 1513 . . . . . 6 (∃𝑣𝑢𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ∃𝑣𝑢((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
56552exbii 1513 . . . . 5 (∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ∃𝑧𝑤𝑣𝑢((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
57 19.42vvvv 1806 . . . . 5 (∃𝑧𝑤𝑣𝑢((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5856, 57bitri 177 . . . 4 (∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡(((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
5953, 58sylibr 141 . . 3 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) → ∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))))
60 3simpb 913 . . . . . . . . 9 ((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) → (𝑓 ∈ (ω × N) ∧ ∈ (ω × N)))
6160adantr 265 . . . . . . . 8 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑓 ∈ (ω × N) ∧ ∈ (ω × N)))
62 simplll 493 . . . . . . . . . 10 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → 𝑓 = ⟨𝑧, 𝑤⟩)
63 simprlr 498 . . . . . . . . . 10 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → = ⟨𝑠, 𝑡⟩)
6462, 63jca 294 . . . . . . . . 9 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩))
6564adantl 266 . . . . . . . 8 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩))
66 oveq1 5546 . . . . . . . . . . . . . . . 16 (𝑣 = ∅ → (𝑣 ·𝑜 𝑡) = (∅ ·𝑜 𝑡))
6763adantl 266 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → = ⟨𝑠, 𝑡⟩)
68 simpl3 920 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ∈ (ω × N))
6967, 68eqeltrrd 2131 . . . . . . . . . . . . . . . . . . . . 21 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ⟨𝑠, 𝑡⟩ ∈ (ω × N))
70 opelxp 4401 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑠, 𝑡⟩ ∈ (ω × N) ↔ (𝑠 ∈ ω ∧ 𝑡N))
7169, 70sylib 131 . . . . . . . . . . . . . . . . . . . 20 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 ∈ ω ∧ 𝑡N))
7271simprd 111 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑡N)
73 pinn 6464 . . . . . . . . . . . . . . . . . . 19 (𝑡N𝑡 ∈ ω)
7472, 73syl 14 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑡 ∈ ω)
75 nnm0r 6088 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ ω → (∅ ·𝑜 𝑡) = ∅)
7674, 75syl 14 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (∅ ·𝑜 𝑡) = ∅)
7776eqeq2d 2067 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑣 ·𝑜 𝑡) = (∅ ·𝑜 𝑡) ↔ (𝑣 ·𝑜 𝑡) = ∅))
7866, 77syl5ib 147 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑣 ·𝑜 𝑡) = ∅))
79 simprr 492 . . . . . . . . . . . . . . . . . 18 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))
80 eqtr2 2074 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔 = ⟨𝑣, 𝑢⟩ ∧ 𝑔 = ⟨𝑎, 𝑏⟩) → ⟨𝑣, 𝑢⟩ = ⟨𝑎, 𝑏⟩)
81 vex 2577 . . . . . . . . . . . . . . . . . . . . . . 23 𝑣 ∈ V
82 vex 2577 . . . . . . . . . . . . . . . . . . . . . . 23 𝑢 ∈ V
8381, 82opth 4001 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑣, 𝑢⟩ = ⟨𝑎, 𝑏⟩ ↔ (𝑣 = 𝑎𝑢 = 𝑏))
8480, 83sylib 131 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔 = ⟨𝑣, 𝑢⟩ ∧ 𝑔 = ⟨𝑎, 𝑏⟩) → (𝑣 = 𝑎𝑢 = 𝑏))
85 oveq1 5546 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = 𝑎 → (𝑣 ·𝑜 𝑡) = (𝑎 ·𝑜 𝑡))
86 oveq1 5546 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = 𝑏 → (𝑢 ·𝑜 𝑠) = (𝑏 ·𝑜 𝑠))
8785, 86eqeqan12d 2071 . . . . . . . . . . . . . . . . . . . . 21 ((𝑣 = 𝑎𝑢 = 𝑏) → ((𝑣 ·𝑜 𝑡) = (𝑢 ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
8884, 87syl 14 . . . . . . . . . . . . . . . . . . . 20 ((𝑔 = ⟨𝑣, 𝑢⟩ ∧ 𝑔 = ⟨𝑎, 𝑏⟩) → ((𝑣 ·𝑜 𝑡) = (𝑢 ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
8988ad2ant2lr 487 . . . . . . . . . . . . . . . . . . 19 (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩)) → ((𝑣 ·𝑜 𝑡) = (𝑢 ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
9089ad2ant2r 486 . . . . . . . . . . . . . . . . . 18 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → ((𝑣 ·𝑜 𝑡) = (𝑢 ·𝑜 𝑠) ↔ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))
9179, 90mpbird 160 . . . . . . . . . . . . . . . . 17 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (𝑣 ·𝑜 𝑡) = (𝑢 ·𝑜 𝑠))
9291eqeq1d 2064 . . . . . . . . . . . . . . . 16 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → ((𝑣 ·𝑜 𝑡) = ∅ ↔ (𝑢 ·𝑜 𝑠) = ∅))
9392adantl 266 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑣 ·𝑜 𝑡) = ∅ ↔ (𝑢 ·𝑜 𝑠) = ∅))
9478, 93sylibd 142 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑢 ·𝑜 𝑠) = ∅))
95 simpllr 494 . . . . . . . . . . . . . . . . . . . 20 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → 𝑔 = ⟨𝑣, 𝑢⟩)
9695adantl 266 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑔 = ⟨𝑣, 𝑢⟩)
97 simpl2 919 . . . . . . . . . . . . . . . . . . 19 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑔 ∈ (ω × N))
9896, 97eqeltrrd 2131 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ⟨𝑣, 𝑢⟩ ∈ (ω × N))
99 opelxp 4401 . . . . . . . . . . . . . . . . . 18 (⟨𝑣, 𝑢⟩ ∈ (ω × N) ↔ (𝑣 ∈ ω ∧ 𝑢N))
10098, 99sylib 131 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 ∈ ω ∧ 𝑢N))
101100simprd 111 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑢N)
102 pinn 6464 . . . . . . . . . . . . . . . 16 (𝑢N𝑢 ∈ ω)
103101, 102syl 14 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑢 ∈ ω)
10471simpld 109 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑠 ∈ ω)
105 nnm00 6132 . . . . . . . . . . . . . . 15 ((𝑢 ∈ ω ∧ 𝑠 ∈ ω) → ((𝑢 ·𝑜 𝑠) = ∅ ↔ (𝑢 = ∅ ∨ 𝑠 = ∅)))
106103, 104, 105syl2anc 397 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑢 ·𝑜 𝑠) = ∅ ↔ (𝑢 = ∅ ∨ 𝑠 = ∅)))
10794, 106sylibd 142 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑢 = ∅ ∨ 𝑠 = ∅)))
108 elni2 6469 . . . . . . . . . . . . . . . 16 (𝑢N ↔ (𝑢 ∈ ω ∧ ∅ ∈ 𝑢))
109108simprbi 264 . . . . . . . . . . . . . . 15 (𝑢N → ∅ ∈ 𝑢)
110101, 109syl 14 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ∅ ∈ 𝑢)
111 n0i 3256 . . . . . . . . . . . . . 14 (∅ ∈ 𝑢 → ¬ 𝑢 = ∅)
112 biorf 673 . . . . . . . . . . . . . 14 𝑢 = ∅ → (𝑠 = ∅ ↔ (𝑢 = ∅ ∨ 𝑠 = ∅)))
113110, 111, 1123syl 17 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 = ∅ ↔ (𝑢 = ∅ ∨ 𝑠 = ∅)))
114107, 113sylibrd 162 . . . . . . . . . . . 12 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → 𝑠 = ∅))
11562adantl 266 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑓 = ⟨𝑧, 𝑤⟩)
116 simpl1 918 . . . . . . . . . . . . . . . . . 18 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑓 ∈ (ω × N))
117115, 116eqeltrrd 2131 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ⟨𝑧, 𝑤⟩ ∈ (ω × N))
118 opelxp 4401 . . . . . . . . . . . . . . . . 17 (⟨𝑧, 𝑤⟩ ∈ (ω × N) ↔ (𝑧 ∈ ω ∧ 𝑤N))
119117, 118sylib 131 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 ∈ ω ∧ 𝑤N))
120119simprd 111 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑤N)
121 pinn 6464 . . . . . . . . . . . . . . 15 (𝑤N𝑤 ∈ ω)
122120, 121syl 14 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑤 ∈ ω)
123 nnm0 6084 . . . . . . . . . . . . . 14 (𝑤 ∈ ω → (𝑤 ·𝑜 ∅) = ∅)
124122, 123syl 14 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑤 ·𝑜 ∅) = ∅)
125 oveq2 5547 . . . . . . . . . . . . . 14 (𝑠 = ∅ → (𝑤 ·𝑜 𝑠) = (𝑤 ·𝑜 ∅))
126125eqeq1d 2064 . . . . . . . . . . . . 13 (𝑠 = ∅ → ((𝑤 ·𝑜 𝑠) = ∅ ↔ (𝑤 ·𝑜 ∅) = ∅))
127124, 126syl5ibrcom 150 . . . . . . . . . . . 12 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 = ∅ → (𝑤 ·𝑜 𝑠) = ∅))
128114, 127syld 44 . . . . . . . . . . 11 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑤 ·𝑜 𝑠) = ∅))
129 oveq2 5547 . . . . . . . . . . . . . . . 16 (𝑣 = ∅ → (𝑤 ·𝑜 𝑣) = (𝑤 ·𝑜 ∅))
130124eqeq2d 2067 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑤 ·𝑜 𝑣) = (𝑤 ·𝑜 ∅) ↔ (𝑤 ·𝑜 𝑣) = ∅))
131129, 130syl5ib 147 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑤 ·𝑜 𝑣) = ∅))
132 simprlr 498 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))
133132eqeq1d 2064 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑧 ·𝑜 𝑢) = ∅ ↔ (𝑤 ·𝑜 𝑣) = ∅))
134131, 133sylibrd 162 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑧 ·𝑜 𝑢) = ∅))
135119simpld 109 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑧 ∈ ω)
136 nnm00 6132 . . . . . . . . . . . . . . 15 ((𝑧 ∈ ω ∧ 𝑢 ∈ ω) → ((𝑧 ·𝑜 𝑢) = ∅ ↔ (𝑧 = ∅ ∨ 𝑢 = ∅)))
137135, 103, 136syl2anc 397 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑧 ·𝑜 𝑢) = ∅ ↔ (𝑧 = ∅ ∨ 𝑢 = ∅)))
138134, 137sylibd 142 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑧 = ∅ ∨ 𝑢 = ∅)))
139 biorf 673 . . . . . . . . . . . . . . 15 𝑢 = ∅ → (𝑧 = ∅ ↔ (𝑢 = ∅ ∨ 𝑧 = ∅)))
140 orcom 657 . . . . . . . . . . . . . . 15 ((𝑢 = ∅ ∨ 𝑧 = ∅) ↔ (𝑧 = ∅ ∨ 𝑢 = ∅))
141139, 140syl6bb 189 . . . . . . . . . . . . . 14 𝑢 = ∅ → (𝑧 = ∅ ↔ (𝑧 = ∅ ∨ 𝑢 = ∅)))
142110, 111, 1413syl 17 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 = ∅ ↔ (𝑧 = ∅ ∨ 𝑢 = ∅)))
143138, 142sylibrd 162 . . . . . . . . . . . 12 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → 𝑧 = ∅))
144 oveq1 5546 . . . . . . . . . . . . . 14 (𝑧 = ∅ → (𝑧 ·𝑜 𝑡) = (∅ ·𝑜 𝑡))
145144eqeq1d 2064 . . . . . . . . . . . . 13 (𝑧 = ∅ → ((𝑧 ·𝑜 𝑡) = ∅ ↔ (∅ ·𝑜 𝑡) = ∅))
14676, 145syl5ibrcom 150 . . . . . . . . . . . 12 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 = ∅ → (𝑧 ·𝑜 𝑡) = ∅))
147143, 146syld 44 . . . . . . . . . . 11 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑧 ·𝑜 𝑡) = ∅))
148128, 147jcad 295 . . . . . . . . . 10 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → ((𝑤 ·𝑜 𝑠) = ∅ ∧ (𝑧 ·𝑜 𝑡) = ∅)))
149 eqtr3 2075 . . . . . . . . . . 11 (((𝑤 ·𝑜 𝑠) = ∅ ∧ (𝑧 ·𝑜 𝑡) = ∅) → (𝑤 ·𝑜 𝑠) = (𝑧 ·𝑜 𝑡))
150149eqcomd 2061 . . . . . . . . . 10 (((𝑤 ·𝑜 𝑠) = ∅ ∧ (𝑧 ·𝑜 𝑡) = ∅) → (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))
151148, 150syl6 33 . . . . . . . . 9 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ → (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)))
152 simplr 490 . . . . . . . . . . . . . . . . 17 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣))
15391, 152oveq12d 5557 . . . . . . . . . . . . . . . 16 ((((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠))) → ((𝑣 ·𝑜 𝑡) ·𝑜 (𝑧 ·𝑜 𝑢)) = ((𝑢 ·𝑜 𝑠) ·𝑜 (𝑤 ·𝑜 𝑣)))
154153adantl 266 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑣 ·𝑜 𝑡) ·𝑜 (𝑧 ·𝑜 𝑢)) = ((𝑢 ·𝑜 𝑠) ·𝑜 (𝑤 ·𝑜 𝑣)))
155100simpld 109 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → 𝑣 ∈ ω)
156 nnmcl 6090 . . . . . . . . . . . . . . . . 17 ((𝑣 ∈ ω ∧ 𝑡 ∈ ω) → (𝑣 ·𝑜 𝑡) ∈ ω)
157155, 74, 156syl2anc 397 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 ·𝑜 𝑡) ∈ ω)
158 nnmcom 6098 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ ω ∧ 𝑑 ∈ ω) → (𝑐 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑐))
159158adantl 266 . . . . . . . . . . . . . . . 16 ((((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ∧ (𝑐 ∈ ω ∧ 𝑑 ∈ ω)) → (𝑐 ·𝑜 𝑑) = (𝑑 ·𝑜 𝑐))
160 nnmass 6096 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ ω ∧ 𝑑 ∈ ω ∧ 𝑒 ∈ ω) → ((𝑐 ·𝑜 𝑑) ·𝑜 𝑒) = (𝑐 ·𝑜 (𝑑 ·𝑜 𝑒)))
161160adantl 266 . . . . . . . . . . . . . . . 16 ((((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ∧ (𝑐 ∈ ω ∧ 𝑑 ∈ ω ∧ 𝑒 ∈ ω)) → ((𝑐 ·𝑜 𝑑) ·𝑜 𝑒) = (𝑐 ·𝑜 (𝑑 ·𝑜 𝑒)))
162157, 135, 103, 159, 161caov13d 5711 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑣 ·𝑜 𝑡) ·𝑜 (𝑧 ·𝑜 𝑢)) = (𝑢 ·𝑜 (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡))))
163 nnmcl 6090 . . . . . . . . . . . . . . . . 17 ((𝑤 ∈ ω ∧ 𝑣 ∈ ω) → (𝑤 ·𝑜 𝑣) ∈ ω)
164122, 155, 163syl2anc 397 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑤 ·𝑜 𝑣) ∈ ω)
165161, 103, 104, 164caovassd 5687 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑢 ·𝑜 𝑠) ·𝑜 (𝑤 ·𝑜 𝑣)) = (𝑢 ·𝑜 (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣))))
166154, 162, 1653eqtr3d 2096 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑢 ·𝑜 (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡))) = (𝑢 ·𝑜 (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣))))
167 nnmcl 6090 . . . . . . . . . . . . . . . 16 ((𝑧 ∈ ω ∧ (𝑣 ·𝑜 𝑡) ∈ ω) → (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡)) ∈ ω)
168135, 157, 167syl2anc 397 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡)) ∈ ω)
169 nnmcl 6090 . . . . . . . . . . . . . . . 16 ((𝑠 ∈ ω ∧ (𝑤 ·𝑜 𝑣) ∈ ω) → (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣)) ∈ ω)
170104, 164, 169syl2anc 397 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣)) ∈ ω)
171 nnmcan 6122 . . . . . . . . . . . . . . 15 (((𝑢 ∈ ω ∧ (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡)) ∈ ω ∧ (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣)) ∈ ω) ∧ ∅ ∈ 𝑢) → ((𝑢 ·𝑜 (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡))) = (𝑢 ·𝑜 (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣))) ↔ (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡)) = (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣))))
172103, 168, 170, 110, 171syl31anc 1149 . . . . . . . . . . . . . 14 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑢 ·𝑜 (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡))) = (𝑢 ·𝑜 (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣))) ↔ (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡)) = (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣))))
173166, 172mpbid 139 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡)) = (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣)))
174135, 155, 74, 159, 161caov12d 5709 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 ·𝑜 (𝑣 ·𝑜 𝑡)) = (𝑣 ·𝑜 (𝑧 ·𝑜 𝑡)))
175104, 122, 155, 159, 161caov13d 5711 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑠 ·𝑜 (𝑤 ·𝑜 𝑣)) = (𝑣 ·𝑜 (𝑤 ·𝑜 𝑠)))
176173, 174, 1753eqtr3d 2096 . . . . . . . . . . . 12 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 ·𝑜 (𝑧 ·𝑜 𝑡)) = (𝑣 ·𝑜 (𝑤 ·𝑜 𝑠)))
177176adantr 265 . . . . . . . . . . 11 ((((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ∧ ∅ ∈ 𝑣) → (𝑣 ·𝑜 (𝑧 ·𝑜 𝑡)) = (𝑣 ·𝑜 (𝑤 ·𝑜 𝑠)))
178 nnmcl 6090 . . . . . . . . . . . . . 14 ((𝑧 ∈ ω ∧ 𝑡 ∈ ω) → (𝑧 ·𝑜 𝑡) ∈ ω)
179135, 74, 178syl2anc 397 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 ·𝑜 𝑡) ∈ ω)
180 nnmcl 6090 . . . . . . . . . . . . . 14 ((𝑤 ∈ ω ∧ 𝑠 ∈ ω) → (𝑤 ·𝑜 𝑠) ∈ ω)
181122, 104, 180syl2anc 397 . . . . . . . . . . . . 13 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑤 ·𝑜 𝑠) ∈ ω)
182155, 179, 1813jca 1095 . . . . . . . . . . . 12 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 ∈ ω ∧ (𝑧 ·𝑜 𝑡) ∈ ω ∧ (𝑤 ·𝑜 𝑠) ∈ ω))
183 nnmcan 6122 . . . . . . . . . . . 12 (((𝑣 ∈ ω ∧ (𝑧 ·𝑜 𝑡) ∈ ω ∧ (𝑤 ·𝑜 𝑠) ∈ ω) ∧ ∅ ∈ 𝑣) → ((𝑣 ·𝑜 (𝑧 ·𝑜 𝑡)) = (𝑣 ·𝑜 (𝑤 ·𝑜 𝑠)) ↔ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)))
184182, 183sylan 271 . . . . . . . . . . 11 ((((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ∧ ∅ ∈ 𝑣) → ((𝑣 ·𝑜 (𝑧 ·𝑜 𝑡)) = (𝑣 ·𝑜 (𝑤 ·𝑜 𝑠)) ↔ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)))
185177, 184mpbid 139 . . . . . . . . . 10 ((((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) ∧ ∅ ∈ 𝑣) → (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))
186185ex 112 . . . . . . . . 9 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (∅ ∈ 𝑣 → (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)))
187 0elnn 4367 . . . . . . . . . 10 (𝑣 ∈ ω → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
188155, 187syl 14 . . . . . . . . 9 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑣 = ∅ ∨ ∅ ∈ 𝑣))
189151, 186, 188mpjaod 648 . . . . . . . 8 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))
19061, 65, 189jca32 297 . . . . . . 7 (((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
1911902eximi 1508 . . . . . 6 (∃𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ∃𝑠𝑡((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
192191exlimivv 1792 . . . . 5 (∃𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ∃𝑠𝑡((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
193192exlimivv 1792 . . . 4 (∃𝑣𝑢𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ∃𝑠𝑡((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
1941932eximi 1508 . . 3 (∃𝑧𝑤𝑣𝑢𝑎𝑏𝑠𝑡((𝑓 ∈ (ω × N) ∧ 𝑔 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑔 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 ·𝑜 𝑢) = (𝑤 ·𝑜 𝑣)) ∧ ((𝑔 = ⟨𝑎, 𝑏⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑎 ·𝑜 𝑡) = (𝑏 ·𝑜 𝑠)))) → ∃𝑧𝑤𝑠𝑡((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
19559, 194syl 14 . 2 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) → ∃𝑧𝑤𝑠𝑡((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
196 19.42vvvv 1806 . . 3 (∃𝑧𝑤𝑠𝑡((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))) ↔ ((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
1975anbi1d 446 . . . . . . 7 (𝑥 = 𝑓 → ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ↔ (𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩)))
198197anbi1d 446 . . . . . 6 (𝑥 = 𝑓 → (((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)) ↔ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
1991984exbidv 1766 . . . . 5 (𝑥 = 𝑓 → (∃𝑧𝑤𝑠𝑡((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)) ↔ ∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
2004, 199anbi12d 450 . . . 4 (𝑥 = 𝑓 → (((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑠𝑡((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))) ↔ ((𝑓 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)))))
20127anbi2d 445 . . . . 5 (𝑦 = → ((𝑓 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ↔ (𝑓 ∈ (ω × N) ∧ ∈ (ω × N))))
20229anbi2d 445 . . . . . . 7 (𝑦 = → ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ↔ (𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩)))
203202anbi1d 446 . . . . . 6 (𝑦 = → (((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)) ↔ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
2042034exbidv 1766 . . . . 5 (𝑦 = → (∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)) ↔ ∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
205201, 204anbi12d 450 . . . 4 (𝑦 = → (((𝑓 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))) ↔ ((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)))))
206 df-enq0 6579 . . . 4 ~Q0 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (ω × N) ∧ 𝑦 ∈ (ω × N)) ∧ ∃𝑧𝑤𝑠𝑡((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠)))}
2071, 19, 200, 205, 206brab 4036 . . 3 (𝑓 ~Q0 ↔ ((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ∃𝑧𝑤𝑠𝑡((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))))
208196, 207bitr4i 180 . 2 (∃𝑧𝑤𝑠𝑡((𝑓 ∈ (ω × N) ∧ ∈ (ω × N)) ∧ ((𝑓 = ⟨𝑧, 𝑤⟩ ∧ = ⟨𝑠, 𝑡⟩) ∧ (𝑧 ·𝑜 𝑡) = (𝑤 ·𝑜 𝑠))) ↔ 𝑓 ~Q0 )
209195, 208sylib 131 1 ((𝑓 ~Q0 𝑔𝑔 ~Q0 ) → 𝑓 ~Q0 )
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 101   ↔ wb 102   ∨ wo 639   ∧ w3a 896   = wceq 1259  ∃wex 1397   ∈ wcel 1409  ∅c0 3251  ⟨cop 3405   class class class wbr 3791  ωcom 4340   × cxp 4370  (class class class)co 5539   ·𝑜 comu 6029  Ncnpi 6427   ~Q0 ceq0 6441 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-13 1420  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-coll 3899  ax-sep 3902  ax-nul 3910  ax-pow 3954  ax-pr 3971  ax-un 4197  ax-setind 4289  ax-iinf 4338 This theorem depends on definitions:  df-bi 114  df-dc 754  df-3or 897  df-3an 898  df-tru 1262  df-fal 1265  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-rex 2329  df-reu 2330  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-dif 2947  df-un 2949  df-in 2951  df-ss 2958  df-nul 3252  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-int 3643  df-iun 3686  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-suc 4135  df-iom 4341  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-ima 4385  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-f1 4934  df-fo 4935  df-f1o 4936  df-fv 4937  df-ov 5542  df-oprab 5543  df-mpt2 5544  df-1st 5794  df-2nd 5795  df-recs 5950  df-irdg 5987  df-oadd 6035  df-omul 6036  df-ni 6459  df-enq0 6579 This theorem is referenced by:  enq0er  6590
 Copyright terms: Public domain W3C validator