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

Theorem sltval2 31053
 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 31044 . 2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
2 fvex 6113 . . . . . . . . . . . . 13 (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
3 fvex 6113 . . . . . . . . . . . . 13 (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
42, 3brtp 30892 . . . . . . . . . . . 12 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜)))
5 1n0 7462 . . . . . . . . . . . . . . . . 17 1𝑜 ≠ ∅
65neii 2784 . . . . . . . . . . . . . . . 16 ¬ 1𝑜 = ∅
7 eqeq1 2614 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 1𝑜 = ∅))
86, 7mtbiri 316 . . . . . . . . . . . . . . 15 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
9 fvprc 6097 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
108, 9nsyl2 141 . . . . . . . . . . . . . 14 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1110adantr 480 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1210adantr 480 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
13 2on0 7456 . . . . . . . . . . . . . . . . 17 2𝑜 ≠ ∅
1413neii 2784 . . . . . . . . . . . . . . . 16 ¬ 2𝑜 = ∅
15 eqeq1 2614 . . . . . . . . . . . . . . . 16 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 → ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 2𝑜 = ∅))
1614, 15mtbiri 316 . . . . . . . . . . . . . . 15 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 → ¬ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
17 fvprc 6097 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
1816, 17nsyl2 141 . . . . . . . . . . . . . 14 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1918adantl 481 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
2011, 12, 193jaoi 1383 . . . . . . . . . . . 12 ((((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1𝑜 ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2𝑜)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
214, 20sylbi 206 . . . . . . . . . . 11 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
22 onintrab 6893 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V ↔ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2321, 22sylib 207 . . . . . . . . . 10 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2423adantl 481 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
25 onelon 5665 . . . . . . . . . . . . . . 15 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ 𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑦 ∈ On)
2625expcom 450 . . . . . . . . . . . . . 14 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On → 𝑦 ∈ On))
2724, 26syl5 33 . . . . . . . . . . . . 13 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → 𝑦 ∈ On))
28 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → (𝐴𝑎) = (𝐴𝑦))
29 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑦 → (𝐵𝑎) = (𝐵𝑦))
3028, 29neeq12d 2843 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑦) ≠ (𝐵𝑦)))
3130onnminsb 6896 . . . . . . . . . . . . . 14 (𝑦 ∈ On → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3231com12 32 . . . . . . . . . . . . 13 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝑦 ∈ On → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3327, 32syld 46 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3433com12 32 . . . . . . . . . . 11 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
35 df-ne 2782 . . . . . . . . . . . 12 ((𝐴𝑦) ≠ (𝐵𝑦) ↔ ¬ (𝐴𝑦) = (𝐵𝑦))
3635con2bii 346 . . . . . . . . . . 11 ((𝐴𝑦) = (𝐵𝑦) ↔ ¬ (𝐴𝑦) ≠ (𝐵𝑦))
3734, 36syl6ibr 241 . . . . . . . . . 10 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐵𝑦)))
3837ralrimiv 2948 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))
3924, 38jca 553 . . . . . . . 8 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
4039ex 449 . . . . . . 7 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))))
4140impac 649 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
42 anass 679 . . . . . 6 ((( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4341, 42sylib 207 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
44 raleq 3115 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ↔ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
45 fveq2 6103 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
46 fveq2 6103 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
4745, 46breq12d 4596 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
4844, 47anbi12d 743 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4948rspcev 3282 . . . . 5 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
5043, 49syl 17 . . . 4 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
5150ex 449 . . 3 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
52 eqeq12 2623 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1𝑜 = ∅))
536, 52mtbiri 316 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) → ¬ (𝐴𝑥) = (𝐵𝑥))
54 1on 7454 . . . . . . . . . . . . . . . . 17 1𝑜 ∈ On
55 0elon 5695 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
56 suc11 5748 . . . . . . . . . . . . . . . . . 18 ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 = suc ∅ ↔ 1𝑜 = ∅))
5756necon3bid 2826 . . . . . . . . . . . . . . . . 17 ((1𝑜 ∈ On ∧ ∅ ∈ On) → (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅))
5854, 55, 57mp2an 704 . . . . . . . . . . . . . . . 16 (suc 1𝑜 ≠ suc ∅ ↔ 1𝑜 ≠ ∅)
595, 58mpbir 220 . . . . . . . . . . . . . . 15 suc 1𝑜 ≠ suc ∅
60 df-2o 7448 . . . . . . . . . . . . . . . 16 2𝑜 = suc 1𝑜
61 df-1o 7447 . . . . . . . . . . . . . . . 16 1𝑜 = suc ∅
6260, 61eqeq12i 2624 . . . . . . . . . . . . . . 15 (2𝑜 = 1𝑜 ↔ suc 1𝑜 = suc ∅)
6359, 62nemtbir 2877 . . . . . . . . . . . . . 14 ¬ 2𝑜 = 1𝑜
64 eqeq12 2623 . . . . . . . . . . . . . . 15 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1𝑜 = 2𝑜))
65 eqcom 2617 . . . . . . . . . . . . . . 15 (1𝑜 = 2𝑜 ↔ 2𝑜 = 1𝑜)
6664, 65syl6bb 275 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ 2𝑜 = 1𝑜))
6763, 66mtbiri 316 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) → ¬ (𝐴𝑥) = (𝐵𝑥))
6813nesymi 2839 . . . . . . . . . . . . . 14 ¬ ∅ = 2𝑜
69 eqeq12 2623 . . . . . . . . . . . . . 14 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜) → ((𝐴𝑥) = (𝐵𝑥) ↔ ∅ = 2𝑜))
7068, 69mtbiri 316 . . . . . . . . . . . . 13 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜) → ¬ (𝐴𝑥) = (𝐵𝑥))
7153, 67, 703jaoi 1383 . . . . . . . . . . . 12 ((((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜)) → ¬ (𝐴𝑥) = (𝐵𝑥))
72 fvex 6113 . . . . . . . . . . . . 13 (𝐴𝑥) ∈ V
73 fvex 6113 . . . . . . . . . . . . 13 (𝐵𝑥) ∈ V
7472, 73brtp 30892 . . . . . . . . . . . 12 ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1𝑜 ∧ (𝐵𝑥) = 2𝑜) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2𝑜)))
75 df-ne 2782 . . . . . . . . . . . 12 ((𝐴𝑥) ≠ (𝐵𝑥) ↔ ¬ (𝐴𝑥) = (𝐵𝑥))
7671, 74, 753imtr4i 280 . . . . . . . . . . 11 ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴𝑥) ≠ (𝐵𝑥))
77 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐴𝑎) = (𝐴𝑥))
78 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐵𝑎) = (𝐵𝑥))
7977, 78neeq12d 2843 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑥) ≠ (𝐵𝑥)))
8079elrab 3331 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)))
8180biimpri 217 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8281adantlr 747 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
83 ssrab2 3650 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On
84 ne0i 3880 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
8584adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
86 onint 6887 . . . . . . . . . . . . . . . . . 18 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8783, 85, 86sylancr 694 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
88 nfrab1 3099 . . . . . . . . . . . . . . . . . . . 20 𝑎{𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
8988nfint 4421 . . . . . . . . . . . . . . . . . . 19 𝑎 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
90 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑎On
91 nfcv 2751 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐴
9291, 89nffv 6110 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
93 nfcv 2751 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐵
9493, 89nffv 6110 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
9592, 94nfne 2882 . . . . . . . . . . . . . . . . . . 19 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
96 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑎) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
97 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑎) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
9896, 97neeq12d 2843 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9989, 90, 95, 98elrabf 3329 . . . . . . . . . . . . . . . . . 18 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
10099simprbi 479 . . . . . . . . . . . . . . . . 17 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
10187, 100syl 17 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
102 df-ne 2782 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
103101, 102sylib 207 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
104 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
105 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑦) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
106104, 105eqeq12d 2625 . . . . . . . . . . . . . . . . 17 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
107106rspccv 3279 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
108107ad2antlr 759 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
109103, 108mtod 188 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥)
110 simpll 786 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 ∈ On)
111 oninton 6892 . . . . . . . . . . . . . . . . 17 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
11283, 84, 111sylancr 694 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
113112adantl 481 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
114 ontri1 5674 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
115110, 113, 114syl2anc 691 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
116109, 115mpbird 246 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
117 intss1 4427 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
118117adantl 481 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
119116, 118eqssd 3585 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
12082, 119syldan 486 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
12176, 120sylan2 490 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
122121fveq2d 6107 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
123121fveq2d 6107 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
124122, 123breq12d 4596 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
125124biimpd 218 . . . . . . 7 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
126125ex 449 . . . . . 6 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
127126pm2.43d 51 . . . . 5 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
128127expimpd 627 . . . 4 (𝑥 ∈ On → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
129128rexlimiv 3009 . . 3 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
13051, 129impbid1 214 . 2 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
1311, 130bitr4d 270 1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∨ w3o 1030   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ⊆ wss 3540  ∅c0 3874  {ctp 4129  ⟨cop 4131  ∩ cint 4410   class class class wbr 4583  Oncon0 5640  suc csuc 5642  ‘cfv 5804  1𝑜c1o 7440  2𝑜c2o 7441   No csur 31037
 Copyright terms: Public domain W3C validator