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 32086
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 32077 . 2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
2 fvex 6350 . . . . . . . . . . . . 13 (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
3 fvex 6350 . . . . . . . . . . . . 13 (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
42, 3brtp 31917 . . . . . . . . . . . 12 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜)))
5 1n0 7732 . . . . . . . . . . . . . . . . 17 1𝑜 ≠ ∅
65neii 2922 . . . . . . . . . . . . . . . 16 ¬ 1𝑜 = ∅
7 eqeq1 2752 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 1𝑜 = ∅))
86, 7mtbiri 316 . . . . . . . . . . . . . . 15 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
9 fvprc 6334 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
108, 9nsyl2 142 . . . . . . . . . . . . . 14 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1110adantr 472 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1210adantr 472 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
13 2on0 7726 . . . . . . . . . . . . . . . . 17 2𝑜 ≠ ∅
1413neii 2922 . . . . . . . . . . . . . . . 16 ¬ 2𝑜 = ∅
15 eqeq1 2752 . . . . . . . . . . . . . . . 16 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 → ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 2𝑜 = ∅))
1614, 15mtbiri 316 . . . . . . . . . . . . . . 15 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 → ¬ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
17 fvprc 6334 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
1816, 17nsyl2 142 . . . . . . . . . . . . . 14 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1918adantl 473 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
2011, 12, 193jaoi 1528 . . . . . . . . . . . 12 ((((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
214, 20sylbi 207 . . . . . . . . . . 11 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
22 onintrab 7154 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V ↔ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2321, 22sylib 208 . . . . . . . . . 10 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2423adantl 473 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
25 onelon 5897 . . . . . . . . . . . . . 14 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ 𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑦 ∈ On)
2625expcom 450 . . . . . . . . . . . . 13 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On → 𝑦 ∈ On))
2724, 26syl5 34 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → 𝑦 ∈ On))
28 fveq2 6340 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐴𝑎) = (𝐴𝑦))
29 fveq2 6340 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐵𝑎) = (𝐵𝑦))
3028, 29neeq12d 2981 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑦) ≠ (𝐵𝑦)))
3130onnminsb 7157 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3231com12 32 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝑦 ∈ On → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3327, 32syldc 48 . . . . . . . . . . 11 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
34 df-ne 2921 . . . . . . . . . . . 12 ((𝐴𝑦) ≠ (𝐵𝑦) ↔ ¬ (𝐴𝑦) = (𝐵𝑦))
3534con2bii 346 . . . . . . . . . . 11 ((𝐴𝑦) = (𝐵𝑦) ↔ ¬ (𝐴𝑦) ≠ (𝐵𝑦))
3633, 35syl6ibr 242 . . . . . . . . . 10 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐵𝑦)))
3736ralrimiv 3091 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))
3824, 37jca 555 . . . . . . . 8 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
3938ex 449 . . . . . . 7 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))))
4039impac 652 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
41 anass 684 . . . . . 6 ((( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4240, 41sylib 208 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
43 raleq 3265 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ↔ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
44 fveq2 6340 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
45 fveq2 6340 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
4644, 45breq12d 4805 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
4743, 46anbi12d 749 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4847rspcev 3437 . . . . 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 449 . . 3 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
51 eqeq12 2761 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1𝑜 = ∅))
526, 51mtbiri 316 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) → ¬ (𝐴𝑥) = (𝐵𝑥))
53 1on 7724 . . . . . . . . . . . . . . . . 17 1𝑜 ∈ On
54 0elon 5927 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
55 suc11 5980 . . . . . . . . . . . . . . . . . 18 ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 = suc ∅ ↔ 1𝑜 = ∅))
5655necon3bid 2964 . . . . . . . . . . . . . . . . 17 ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅))
5753, 54, 56mp2an 710 . . . . . . . . . . . . . . . 16 (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅)
585, 57mpbir 221 . . . . . . . . . . . . . . 15 suc 1𝑜 ≠ suc ∅
59 df-2o 7718 . . . . . . . . . . . . . . . 16 2𝑜 = suc 1𝑜
60 df-1o 7717 . . . . . . . . . . . . . . . 16 1𝑜 = suc ∅
6159, 60eqeq12i 2762 . . . . . . . . . . . . . . 15 (2𝑜 = 1𝑜 ↔ suc 1𝑜 = suc ∅)
6258, 61nemtbir 3015 . . . . . . . . . . . . . 14 ¬ 2𝑜 = 1𝑜
63 eqeq12 2761 . . . . . . . . . . . . . . 15 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1𝑜 = 2𝑜))
64 eqcom 2755 . . . . . . . . . . . . . . 15 (1𝑜 = 2𝑜 ↔ 2𝑜 = 1𝑜)
6563, 64syl6bb 276 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ 2𝑜 = 1𝑜))
6662, 65mtbiri 316 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ¬ (𝐴𝑥) = (𝐵𝑥))
6713nesymi 2977 . . . . . . . . . . . . . 14 ¬ ∅ = 2𝑜
68 eqeq12 2761 . . . . . . . . . . . . . 14 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ ∅ = 2𝑜))
6967, 68mtbiri 316 . . . . . . . . . . . . 13 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜) → ¬ (𝐴𝑥) = (𝐵𝑥))
7052, 66, 693jaoi 1528 . . . . . . . . . . . 12 ((((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜)) → ¬ (𝐴𝑥) = (𝐵𝑥))
71 fvex 6350 . . . . . . . . . . . . 13 (𝐴𝑥) ∈ V
72 fvex 6350 . . . . . . . . . . . . 13 (𝐵𝑥) ∈ V
7371, 72brtp 31917 . . . . . . . . . . . 12 ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜)))
74 df-ne 2921 . . . . . . . . . . . 12 ((𝐴𝑥) ≠ (𝐵𝑥) ↔ ¬ (𝐴𝑥) = (𝐵𝑥))
7570, 73, 743imtr4i 281 . . . . . . . . . . 11 ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴𝑥) ≠ (𝐵𝑥))
76 fveq2 6340 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐴𝑎) = (𝐴𝑥))
77 fveq2 6340 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐵𝑎) = (𝐵𝑥))
7876, 77neeq12d 2981 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑥) ≠ (𝐵𝑥)))
7978elrab 3492 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)))
8079biimpri 218 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8180adantlr 753 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
82 ssrab2 3816 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On
83 ne0i 4052 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
8483adantl 473 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
85 onint 7148 . . . . . . . . . . . . . . . . . 18 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8682, 84, 85sylancr 698 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
87 nfrab1 3249 . . . . . . . . . . . . . . . . . . . 20 𝑎{𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
8887nfint 4626 . . . . . . . . . . . . . . . . . . 19 𝑎 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
89 nfcv 2890 . . . . . . . . . . . . . . . . . . 19 𝑎On
90 nfcv 2890 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐴
9190, 88nffv 6347 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
92 nfcv 2890 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐵
9392, 88nffv 6347 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
9491, 93nfne 3020 . . . . . . . . . . . . . . . . . . 19 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
95 fveq2 6340 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑎) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
96 fveq2 6340 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑎) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
9795, 96neeq12d 2981 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9888, 89, 94, 97elrabf 3488 . . . . . . . . . . . . . . . . . 18 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9998simprbi 483 . . . . . . . . . . . . . . . . 17 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
10086, 99syl 17 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
101 df-ne 2921 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
102100, 101sylib 208 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
103 fveq2 6340 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
104 fveq2 6340 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑦) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
105103, 104eqeq12d 2763 . . . . . . . . . . . . . . . . 17 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
106105rspccv 3434 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
107106ad2antlr 765 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
108102, 107mtod 189 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥)
109 simpll 807 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 ∈ On)
110 oninton 7153 . . . . . . . . . . . . . . . . 17 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
11182, 83, 110sylancr 698 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
112111adantl 473 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
113 ontri1 5906 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
114109, 112, 113syl2anc 696 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
115108, 114mpbird 247 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
116 intss1 4632 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
117116adantl 473 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
118115, 117eqssd 3749 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
11981, 118syldan 488 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
12075, 119sylan2 492 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
121120fveq2d 6344 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
122120fveq2d 6344 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
123121, 122breq12d 4805 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
124123biimpd 219 . . . . . . 7 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
125124ex 449 . . . . . 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 630 . . . 4 (𝑥 ∈ On → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
128127rexlimiv 3153 . . 3 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
12950, 128impbid1 215 . 2 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
1301, 129bitr4d 271 1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3o 1071   = wceq 1620  wcel 2127  wne 2920  wral 3038  wrex 3039  {crab 3042  Vcvv 3328  wss 3703  c0 4046  {ctp 4313  cop 4315   cint 4615   class class class wbr 4792  Oncon0 5872  suc csuc 5874  cfv 6037  1𝑜c1o 7710  2𝑜c2o 7711   No csur 32070   <s cslt 32071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-br 4793  df-opab 4853  df-tr 4893  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-ord 5875  df-on 5876  df-suc 5878  df-iota 6000  df-fv 6045  df-1o 7717  df-2o 7718  df-slt 32074
This theorem is referenced by:  sltintdifex  32091  sltres  32092  noextendlt  32099  noextendgt  32100  nosepnelem  32107  nosep1o  32109  nosepdmlem  32110  nodenselem8  32118  nosupbnd2lem1  32138
  Copyright terms: Public domain W3C validator