Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sltval2 Structured version   Visualization version   GIF version

Theorem sltval2 32128
Description: Alternate expression for surreal less than. Two surreals obey surreal less than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.)
Assertion
Ref Expression
sltval2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
Distinct variable groups:   𝐴,𝑎   𝐵,𝑎

Proof of Theorem sltval2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sltval 32119 . 2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
2 fvex 6417 . . . . . . . . . . . . 13 (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
3 fvex 6417 . . . . . . . . . . . . 13 (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
42, 3brtp 31959 . . . . . . . . . . . 12 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜)))
5 1n0 7808 . . . . . . . . . . . . . . . . 17 1𝑜 ≠ ∅
65neii 2980 . . . . . . . . . . . . . . . 16 ¬ 1𝑜 = ∅
7 eqeq1 2810 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 1𝑜 = ∅))
86, 7mtbiri 318 . . . . . . . . . . . . . . 15 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
9 fvprc 6397 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
108, 9nsyl2 144 . . . . . . . . . . . . . 14 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1110adantr 468 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1210adantr 468 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
13 2on0 7802 . . . . . . . . . . . . . . . . 17 2𝑜 ≠ ∅
1413neii 2980 . . . . . . . . . . . . . . . 16 ¬ 2𝑜 = ∅
15 eqeq1 2810 . . . . . . . . . . . . . . . 16 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 → ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 2𝑜 = ∅))
1614, 15mtbiri 318 . . . . . . . . . . . . . . 15 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 → ¬ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
17 fvprc 6397 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
1816, 17nsyl2 144 . . . . . . . . . . . . . 14 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1918adantl 469 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
2011, 12, 193jaoi 1545 . . . . . . . . . . . 12 ((((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
214, 20sylbi 208 . . . . . . . . . . 11 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
22 onintrab 7227 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V ↔ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2321, 22sylib 209 . . . . . . . . . 10 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2423adantl 469 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
25 onelon 5961 . . . . . . . . . . . . . 14 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ 𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑦 ∈ On)
2625expcom 400 . . . . . . . . . . . . 13 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On → 𝑦 ∈ On))
2724, 26syl5 34 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → 𝑦 ∈ On))
28 fveq2 6404 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐴𝑎) = (𝐴𝑦))
29 fveq2 6404 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐵𝑎) = (𝐵𝑦))
3028, 29neeq12d 3039 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑦) ≠ (𝐵𝑦)))
3130onnminsb 7230 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3231com12 32 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝑦 ∈ On → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3327, 32syldc 48 . . . . . . . . . . 11 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
34 df-ne 2979 . . . . . . . . . . . 12 ((𝐴𝑦) ≠ (𝐵𝑦) ↔ ¬ (𝐴𝑦) = (𝐵𝑦))
3534con2bii 348 . . . . . . . . . . 11 ((𝐴𝑦) = (𝐵𝑦) ↔ ¬ (𝐴𝑦) ≠ (𝐵𝑦))
3633, 35syl6ibr 243 . . . . . . . . . 10 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐵𝑦)))
3736ralrimiv 3153 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))
3824, 37jca 503 . . . . . . . 8 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
3938ex 399 . . . . . . 7 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))))
4039impac 544 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
41 anass 456 . . . . . 6 ((( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4240, 41sylib 209 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
43 raleq 3327 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ↔ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
44 fveq2 6404 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
45 fveq2 6404 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
4644, 45breq12d 4857 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
4743, 46anbi12d 618 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4847rspcev 3502 . . . . 5 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
4942, 48syl 17 . . . 4 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
5049ex 399 . . 3 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
51 eqeq12 2819 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1𝑜 = ∅))
526, 51mtbiri 318 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) → ¬ (𝐴𝑥) = (𝐵𝑥))
53 1on 7799 . . . . . . . . . . . . . . . . 17 1𝑜 ∈ On
54 0elon 5990 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
55 suc11 6040 . . . . . . . . . . . . . . . . . 18 ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 = suc ∅ ↔ 1𝑜 = ∅))
5655necon3bid 3022 . . . . . . . . . . . . . . . . 17 ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅))
5753, 54, 56mp2an 675 . . . . . . . . . . . . . . . 16 (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅)
585, 57mpbir 222 . . . . . . . . . . . . . . 15 suc 1𝑜 ≠ suc ∅
59 df-2o 7793 . . . . . . . . . . . . . . . 16 2𝑜 = suc 1𝑜
60 df-1o 7792 . . . . . . . . . . . . . . . 16 1𝑜 = suc ∅
6159, 60eqeq12i 2820 . . . . . . . . . . . . . . 15 (2𝑜 = 1𝑜 ↔ suc 1𝑜 = suc ∅)
6258, 61nemtbir 3073 . . . . . . . . . . . . . 14 ¬ 2𝑜 = 1𝑜
63 eqeq12 2819 . . . . . . . . . . . . . . 15 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1𝑜 = 2𝑜))
64 eqcom 2813 . . . . . . . . . . . . . . 15 (1𝑜 = 2𝑜 ↔ 2𝑜 = 1𝑜)
6563, 64syl6bb 278 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ 2𝑜 = 1𝑜))
6662, 65mtbiri 318 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ¬ (𝐴𝑥) = (𝐵𝑥))
6713nesymi 3035 . . . . . . . . . . . . . 14 ¬ ∅ = 2𝑜
68 eqeq12 2819 . . . . . . . . . . . . . 14 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ ∅ = 2𝑜))
6967, 68mtbiri 318 . . . . . . . . . . . . 13 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜) → ¬ (𝐴𝑥) = (𝐵𝑥))
7052, 66, 693jaoi 1545 . . . . . . . . . . . 12 ((((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜)) → ¬ (𝐴𝑥) = (𝐵𝑥))
71 fvex 6417 . . . . . . . . . . . . 13 (𝐴𝑥) ∈ V
72 fvex 6417 . . . . . . . . . . . . 13 (𝐵𝑥) ∈ V
7371, 72brtp 31959 . . . . . . . . . . . 12 ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜)))
74 df-ne 2979 . . . . . . . . . . . 12 ((𝐴𝑥) ≠ (𝐵𝑥) ↔ ¬ (𝐴𝑥) = (𝐵𝑥))
7570, 73, 743imtr4i 283 . . . . . . . . . . 11 ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴𝑥) ≠ (𝐵𝑥))
76 fveq2 6404 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐴𝑎) = (𝐴𝑥))
77 fveq2 6404 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐵𝑎) = (𝐵𝑥))
7876, 77neeq12d 3039 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑥) ≠ (𝐵𝑥)))
7978elrab 3559 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)))
8079biimpri 219 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8180adantlr 697 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
82 ssrab2 3884 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On
83 ne0i 4122 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
8483adantl 469 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
85 onint 7221 . . . . . . . . . . . . . . . . . 18 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8682, 84, 85sylancr 577 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
87 nfrab1 3311 . . . . . . . . . . . . . . . . . . . 20 𝑎{𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
8887nfint 4679 . . . . . . . . . . . . . . . . . . 19 𝑎 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
89 nfcv 2948 . . . . . . . . . . . . . . . . . . 19 𝑎On
90 nfcv 2948 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐴
9190, 88nffv 6414 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
92 nfcv 2948 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐵
9392, 88nffv 6414 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
9491, 93nfne 3078 . . . . . . . . . . . . . . . . . . 19 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
95 fveq2 6404 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑎) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
96 fveq2 6404 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑎) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
9795, 96neeq12d 3039 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9888, 89, 94, 97elrabf 3555 . . . . . . . . . . . . . . . . . 18 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9998simprbi 486 . . . . . . . . . . . . . . . . 17 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
10086, 99syl 17 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
101 df-ne 2979 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
102100, 101sylib 209 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
103 fveq2 6404 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
104 fveq2 6404 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑦) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
105103, 104eqeq12d 2821 . . . . . . . . . . . . . . . . 17 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
106105rspccv 3499 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
107106ad2antlr 709 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
108102, 107mtod 189 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥)
109 simpll 774 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 ∈ On)
110 oninton 7226 . . . . . . . . . . . . . . . . 17 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
11182, 83, 110sylancr 577 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
112111adantl 469 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
113 ontri1 5970 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
114109, 112, 113syl2anc 575 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
115108, 114mpbird 248 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
116 intss1 4684 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
117116adantl 469 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
118115, 117eqssd 3815 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
11981, 118syldan 581 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
12075, 119sylan2 582 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
121120fveq2d 6408 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
122120fveq2d 6408 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
123121, 122breq12d 4857 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
124123biimpd 220 . . . . . . 7 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
125124ex 399 . . . . . 6 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
126125pm2.43d 53 . . . . 5 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
127126expimpd 443 . . . 4 (𝑥 ∈ On → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
128127rexlimiv 3215 . . 3 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
12950, 128impbid1 216 . 2 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
1301, 129bitr4d 273 1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3o 1099   = wceq 1637  wcel 2156  wne 2978  wral 3096  wrex 3097  {crab 3100  Vcvv 3391  wss 3769  c0 4116  {ctp 4374  cop 4376   cint 4669   class class class wbr 4844  Oncon0 5936  suc csuc 5938  cfv 6097  1𝑜c1o 7785  2𝑜c2o 7786   No csur 32112   <s cslt 32113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-br 4845  df-opab 4907  df-tr 4947  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-ord 5939  df-on 5940  df-suc 5942  df-iota 6060  df-fv 6105  df-1o 7792  df-2o 7793  df-slt 32116
This theorem is referenced by:  sltintdifex  32133  sltres  32134  noextendlt  32141  noextendgt  32142  nosepnelem  32149  nosep1o  32151  nosepdmlem  32152  nodenselem8  32160  nosupbnd2lem1  32180
  Copyright terms: Public domain W3C validator