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 33060
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 ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
Distinct variable groups:   𝐴,𝑎   𝐵,𝑎

Proof of Theorem sltval2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sltval 33051 . 2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
2 fvex 6676 . . . . . . . . . . . . 13 (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
3 fvex 6676 . . . . . . . . . . . . 13 (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
42, 3brtp 32882 . . . . . . . . . . . 12 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o)))
5 1n0 8108 . . . . . . . . . . . . . . . . 17 1o ≠ ∅
65neii 3015 . . . . . . . . . . . . . . . 16 ¬ 1o = ∅
7 eqeq1 2822 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 1o = ∅))
86, 7mtbiri 328 . . . . . . . . . . . . . . 15 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
9 fvprc 6656 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
108, 9nsyl2 143 . . . . . . . . . . . . . 14 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1110adantr 481 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1210adantr 481 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
13 2on0 8102 . . . . . . . . . . . . . . . . 17 2o ≠ ∅
1413neii 3015 . . . . . . . . . . . . . . . 16 ¬ 2o = ∅
15 eqeq1 2822 . . . . . . . . . . . . . . . 16 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o → ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 2o = ∅))
1614, 15mtbiri 328 . . . . . . . . . . . . . . 15 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o → ¬ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
17 fvprc 6656 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
1816, 17nsyl2 143 . . . . . . . . . . . . . 14 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1918adantl 482 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
2011, 12, 193jaoi 1419 . . . . . . . . . . . 12 ((((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
214, 20sylbi 218 . . . . . . . . . . 11 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
22 onintrab 7505 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V ↔ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2321, 22sylib 219 . . . . . . . . . 10 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2423adantl 482 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
25 onelon 6209 . . . . . . . . . . . . . 14 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ 𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑦 ∈ On)
2625expcom 414 . . . . . . . . . . . . 13 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On → 𝑦 ∈ On))
2724, 26syl5 34 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → 𝑦 ∈ On))
28 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐴𝑎) = (𝐴𝑦))
29 fveq2 6663 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐵𝑎) = (𝐵𝑦))
3028, 29neeq12d 3074 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑦) ≠ (𝐵𝑦)))
3130onnminsb 7508 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3231com12 32 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝑦 ∈ On → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3327, 32syldc 48 . . . . . . . . . . 11 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
34 df-ne 3014 . . . . . . . . . . . 12 ((𝐴𝑦) ≠ (𝐵𝑦) ↔ ¬ (𝐴𝑦) = (𝐵𝑦))
3534con2bii 359 . . . . . . . . . . 11 ((𝐴𝑦) = (𝐵𝑦) ↔ ¬ (𝐴𝑦) ≠ (𝐵𝑦))
3633, 35syl6ibr 253 . . . . . . . . . 10 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐵𝑦)))
3736ralrimiv 3178 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))
3824, 37jca 512 . . . . . . . 8 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
3938ex 413 . . . . . . 7 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))))
4039impac 553 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
41 anass 469 . . . . . 6 ((( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4240, 41sylib 219 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
43 raleq 3403 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ↔ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
44 fveq2 6663 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
45 fveq2 6663 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
4644, 45breq12d 5070 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
4743, 46anbi12d 630 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4847rspcev 3620 . . . . 5 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
4942, 48syl 17 . . . 4 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
5049ex 413 . . 3 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
51 eqeq12 2832 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1o = ∅))
526, 51mtbiri 328 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) → ¬ (𝐴𝑥) = (𝐵𝑥))
53 1on 8098 . . . . . . . . . . . . . . . . 17 1o ∈ On
54 0elon 6237 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
55 suc11 6287 . . . . . . . . . . . . . . . . . 18 ((1o ∈ On ∧ ∅ ∈ On) → (suc 1o = suc ∅ ↔ 1o = ∅))
5655necon3bid 3057 . . . . . . . . . . . . . . . . 17 ((1o ∈ On ∧ ∅ ∈ On) → (suc 1o ≠ suc ∅ ↔ 1o ≠ ∅))
5753, 54, 56mp2an 688 . . . . . . . . . . . . . . . 16 (suc 1o ≠ suc ∅ ↔ 1o ≠ ∅)
585, 57mpbir 232 . . . . . . . . . . . . . . 15 suc 1o ≠ suc ∅
59 df-2o 8092 . . . . . . . . . . . . . . . 16 2o = suc 1o
60 df-1o 8091 . . . . . . . . . . . . . . . 16 1o = suc ∅
6159, 60eqeq12i 2833 . . . . . . . . . . . . . . 15 (2o = 1o ↔ suc 1o = suc ∅)
6258, 61nemtbir 3109 . . . . . . . . . . . . . 14 ¬ 2o = 1o
63 eqeq12 2832 . . . . . . . . . . . . . . 15 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1o = 2o))
64 eqcom 2825 . . . . . . . . . . . . . . 15 (1o = 2o ↔ 2o = 1o)
6563, 64syl6bb 288 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) → ((𝐴𝑥) = (𝐵𝑥) ↔ 2o = 1o))
6662, 65mtbiri 328 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) → ¬ (𝐴𝑥) = (𝐵𝑥))
6713nesymi 3070 . . . . . . . . . . . . . 14 ¬ ∅ = 2o
68 eqeq12 2832 . . . . . . . . . . . . . 14 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o) → ((𝐴𝑥) = (𝐵𝑥) ↔ ∅ = 2o))
6967, 68mtbiri 328 . . . . . . . . . . . . 13 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o) → ¬ (𝐴𝑥) = (𝐵𝑥))
7052, 66, 693jaoi 1419 . . . . . . . . . . . 12 ((((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o)) → ¬ (𝐴𝑥) = (𝐵𝑥))
71 fvex 6676 . . . . . . . . . . . . 13 (𝐴𝑥) ∈ V
72 fvex 6676 . . . . . . . . . . . . 13 (𝐵𝑥) ∈ V
7371, 72brtp 32882 . . . . . . . . . . . 12 ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o)))
74 df-ne 3014 . . . . . . . . . . . 12 ((𝐴𝑥) ≠ (𝐵𝑥) ↔ ¬ (𝐴𝑥) = (𝐵𝑥))
7570, 73, 743imtr4i 293 . . . . . . . . . . 11 ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) → (𝐴𝑥) ≠ (𝐵𝑥))
76 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐴𝑎) = (𝐴𝑥))
77 fveq2 6663 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐵𝑎) = (𝐵𝑥))
7876, 77neeq12d 3074 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑥) ≠ (𝐵𝑥)))
7978elrab 3677 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)))
8079biimpri 229 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8180adantlr 711 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
82 ssrab2 4053 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On
83 ne0i 4297 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
8483adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
85 onint 7499 . . . . . . . . . . . . . . . . . 18 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8682, 84, 85sylancr 587 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
87 nfrab1 3382 . . . . . . . . . . . . . . . . . . . 20 𝑎{𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
8887nfint 4877 . . . . . . . . . . . . . . . . . . 19 𝑎 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
89 nfcv 2974 . . . . . . . . . . . . . . . . . . 19 𝑎On
90 nfcv 2974 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐴
9190, 88nffv 6673 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
92 nfcv 2974 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐵
9392, 88nffv 6673 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
9491, 93nfne 3116 . . . . . . . . . . . . . . . . . . 19 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
95 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑎) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
96 fveq2 6663 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑎) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
9795, 96neeq12d 3074 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9888, 89, 94, 97elrabf 3673 . . . . . . . . . . . . . . . . . 18 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9998simprbi 497 . . . . . . . . . . . . . . . . 17 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
10086, 99syl 17 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
101 df-ne 3014 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
102100, 101sylib 219 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
103 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
104 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑦) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
105103, 104eqeq12d 2834 . . . . . . . . . . . . . . . . 17 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
106105rspccv 3617 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
107106ad2antlr 723 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
108102, 107mtod 199 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥)
109 simpll 763 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 ∈ On)
110 oninton 7504 . . . . . . . . . . . . . . . . 17 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
11182, 83, 110sylancr 587 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
112111adantl 482 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
113 ontri1 6218 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
114109, 112, 113syl2anc 584 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
115108, 114mpbird 258 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
116 intss1 4882 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
117116adantl 482 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
118115, 117eqssd 3981 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
11981, 118syldan 591 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
12075, 119sylan2 592 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
121120fveq2d 6667 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
122120fveq2d 6667 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
123121, 122breq12d 5070 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
124123biimpd 230 . . . . . . 7 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
125124ex 413 . . . . . 6 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
126125pm2.43d 53 . . . . 5 ((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
127126expimpd 454 . . . 4 (𝑥 ∈ On → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
128127rexlimiv 3277 . . 3 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
12950, 128impbid1 226 . 2 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
1301, 129bitr4d 283 1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3o 1078   = wceq 1528  wcel 2105  wne 3013  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  wss 3933  c0 4288  {ctp 4561  cop 4563   cint 4867   class class class wbr 5057  Oncon0 6184  suc csuc 6186  cfv 6348  1oc1o 8084  2oc2o 8085   No csur 33044   <s cslt 33045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-br 5058  df-opab 5120  df-tr 5164  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-ord 6187  df-on 6188  df-suc 6190  df-iota 6307  df-fv 6356  df-1o 8091  df-2o 8092  df-slt 33048
This theorem is referenced by:  sltintdifex  33065  sltres  33066  noextendlt  33073  noextendgt  33074  nosepnelem  33081  nosep1o  33083  nosepdmlem  33084  nodenselem8  33092  nosupbnd2lem1  33112
  Copyright terms: Public domain W3C validator