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 33629
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 33620 . 2 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
2 fvex 6751 . . . . . . . . . . . . 13 (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
3 fvex 6751 . . . . . . . . . . . . 13 (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ∈ V
42, 3brtp 33466 . . . . . . . . . . . 12 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o)))
5 1n0 8244 . . . . . . . . . . . . . . . . 17 1o ≠ ∅
65neii 2945 . . . . . . . . . . . . . . . 16 ¬ 1o = ∅
7 eqeq1 2743 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 1o = ∅))
86, 7mtbiri 330 . . . . . . . . . . . . . . 15 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
9 fvprc 6730 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
108, 9nsyl2 143 . . . . . . . . . . . . . 14 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1110adantr 484 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1210adantr 484 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
13 2on0 8234 . . . . . . . . . . . . . . . . 17 2o ≠ ∅
1413neii 2945 . . . . . . . . . . . . . . . 16 ¬ 2o = ∅
15 eqeq1 2743 . . . . . . . . . . . . . . . 16 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o → ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ↔ 2o = ∅))
1614, 15mtbiri 330 . . . . . . . . . . . . . . 15 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o → ¬ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
17 fvprc 6730 . . . . . . . . . . . . . . 15 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V → (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅)
1816, 17nsyl2 143 . . . . . . . . . . . . . 14 ((𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
1918adantl 485 . . . . . . . . . . . . 13 (((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
2011, 12, 193jaoi 1429 . . . . . . . . . . . 12 ((((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 1o ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o) ∨ ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = ∅ ∧ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = 2o)) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
214, 20sylbi 220 . . . . . . . . . . 11 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V)
22 onintrab 7601 . . . . . . . . . . 11 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ V ↔ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2321, 22sylib 221 . . . . . . . . . 10 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
2423adantl 485 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
25 onelon 6258 . . . . . . . . . . . . . 14 (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ 𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑦 ∈ On)
2625expcom 417 . . . . . . . . . . . . 13 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On → 𝑦 ∈ On))
2724, 26syl5 34 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → 𝑦 ∈ On))
28 fveq2 6738 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐴𝑎) = (𝐴𝑦))
29 fveq2 6738 . . . . . . . . . . . . . . 15 (𝑎 = 𝑦 → (𝐵𝑎) = (𝐵𝑦))
3028, 29neeq12d 3005 . . . . . . . . . . . . . 14 (𝑎 = 𝑦 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑦) ≠ (𝐵𝑦)))
3130onnminsb 7604 . . . . . . . . . . . . 13 (𝑦 ∈ On → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3231com12 32 . . . . . . . . . . . 12 (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝑦 ∈ On → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
3327, 32syldc 48 . . . . . . . . . . 11 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ¬ (𝐴𝑦) ≠ (𝐵𝑦)))
34 df-ne 2944 . . . . . . . . . . . 12 ((𝐴𝑦) ≠ (𝐵𝑦) ↔ ¬ (𝐴𝑦) = (𝐵𝑦))
3534con2bii 361 . . . . . . . . . . 11 ((𝐴𝑦) = (𝐵𝑦) ↔ ¬ (𝐴𝑦) ≠ (𝐵𝑦))
3633, 35syl6ibr 255 . . . . . . . . . 10 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐵𝑦)))
3736ralrimiv 3107 . . . . . . . . 9 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))
3824, 37jca 515 . . . . . . . 8 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
3938ex 416 . . . . . . 7 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦))))
4039impac 556 . . . . . 6 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → (( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
41 anass 472 . . . . . 6 ((( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4240, 41sylib 221 . . . . 5 (((𝐴 No 𝐵 No ) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
43 raleq 3334 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ↔ ∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦)))
44 fveq2 6738 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
45 fveq2 6738 . . . . . . . 8 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
4644, 45breq12d 5082 . . . . . . 7 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
4743, 46anbi12d 634 . . . . . 6 (𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ (∀𝑦 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))))
4847rspcev 3552 . . . . 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 416 . . 3 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
51 eqeq12 2756 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1o = ∅))
526, 51mtbiri 330 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) → ¬ (𝐴𝑥) = (𝐵𝑥))
53 1on 8232 . . . . . . . . . . . . . . . . 17 1o ∈ On
54 0elon 6286 . . . . . . . . . . . . . . . . 17 ∅ ∈ On
55 suc11 6336 . . . . . . . . . . . . . . . . . 18 ((1o ∈ On ∧ ∅ ∈ On) → (suc 1o = suc ∅ ↔ 1o = ∅))
5655necon3bid 2988 . . . . . . . . . . . . . . . . 17 ((1o ∈ On ∧ ∅ ∈ On) → (suc 1o ≠ suc ∅ ↔ 1o ≠ ∅))
5753, 54, 56mp2an 692 . . . . . . . . . . . . . . . 16 (suc 1o ≠ suc ∅ ↔ 1o ≠ ∅)
585, 57mpbir 234 . . . . . . . . . . . . . . 15 suc 1o ≠ suc ∅
59 df-2o 8226 . . . . . . . . . . . . . . . 16 2o = suc 1o
60 df-1o 8225 . . . . . . . . . . . . . . . 16 1o = suc ∅
6159, 60eqeq12i 2757 . . . . . . . . . . . . . . 15 (2o = 1o ↔ suc 1o = suc ∅)
6258, 61nemtbir 3040 . . . . . . . . . . . . . 14 ¬ 2o = 1o
63 eqeq12 2756 . . . . . . . . . . . . . . 15 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) → ((𝐴𝑥) = (𝐵𝑥) ↔ 1o = 2o))
64 eqcom 2746 . . . . . . . . . . . . . . 15 (1o = 2o ↔ 2o = 1o)
6563, 64bitrdi 290 . . . . . . . . . . . . . 14 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) → ((𝐴𝑥) = (𝐵𝑥) ↔ 2o = 1o))
6662, 65mtbiri 330 . . . . . . . . . . . . 13 (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) → ¬ (𝐴𝑥) = (𝐵𝑥))
6713nesymi 3001 . . . . . . . . . . . . . 14 ¬ ∅ = 2o
68 eqeq12 2756 . . . . . . . . . . . . . 14 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o) → ((𝐴𝑥) = (𝐵𝑥) ↔ ∅ = 2o))
6967, 68mtbiri 330 . . . . . . . . . . . . 13 (((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o) → ¬ (𝐴𝑥) = (𝐵𝑥))
7052, 66, 693jaoi 1429 . . . . . . . . . . . 12 ((((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o)) → ¬ (𝐴𝑥) = (𝐵𝑥))
71 fvex 6751 . . . . . . . . . . . . 13 (𝐴𝑥) ∈ V
72 fvex 6751 . . . . . . . . . . . . 13 (𝐵𝑥) ∈ V
7371, 72brtp 33466 . . . . . . . . . . . 12 ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (((𝐴𝑥) = 1o ∧ (𝐵𝑥) = ∅) ∨ ((𝐴𝑥) = 1o ∧ (𝐵𝑥) = 2o) ∨ ((𝐴𝑥) = ∅ ∧ (𝐵𝑥) = 2o)))
74 df-ne 2944 . . . . . . . . . . . 12 ((𝐴𝑥) ≠ (𝐵𝑥) ↔ ¬ (𝐴𝑥) = (𝐵𝑥))
7570, 73, 743imtr4i 295 . . . . . . . . . . 11 ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) → (𝐴𝑥) ≠ (𝐵𝑥))
76 fveq2 6738 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐴𝑎) = (𝐴𝑥))
77 fveq2 6738 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → (𝐵𝑎) = (𝐵𝑥))
7876, 77neeq12d 3005 . . . . . . . . . . . . . . 15 (𝑎 = 𝑥 → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴𝑥) ≠ (𝐵𝑥)))
7978elrab 3617 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ (𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)))
8079biimpri 231 . . . . . . . . . . . . 13 ((𝑥 ∈ On ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8180adantlr 715 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
82 ssrab2 4009 . . . . . . . . . . . . . . . . . 18 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On
83 ne0i 4265 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
8483adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅)
85 onint 7595 . . . . . . . . . . . . . . . . . 18 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
8682, 84, 85sylancr 590 . . . . . . . . . . . . . . . . 17 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
87 nfrab1 3311 . . . . . . . . . . . . . . . . . . . 20 𝑎{𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
8887nfint 4885 . . . . . . . . . . . . . . . . . . 19 𝑎 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}
89 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑎On
90 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐴
9190, 88nffv 6748 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
92 nfcv 2907 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐵
9392, 88nffv 6748 . . . . . . . . . . . . . . . . . . . 20 𝑎(𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
9491, 93nfne 3045 . . . . . . . . . . . . . . . . . . 19 𝑎(𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
95 fveq2 6738 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑎) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
96 fveq2 6738 . . . . . . . . . . . . . . . . . . . 20 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑎) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
9795, 96neeq12d 3005 . . . . . . . . . . . . . . . . . . 19 (𝑎 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑎) ≠ (𝐵𝑎) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9888, 89, 94, 97elrabf 3613 . . . . . . . . . . . . . . . . . 18 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On ∧ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
9998simprbi 500 . . . . . . . . . . . . . . . . 17 ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
10086, 99syl 17 . . . . . . . . . . . . . . . 16 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
101 df-ne 2944 . . . . . . . . . . . . . . . 16 ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ≠ (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
102100, 101sylib 221 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
103 fveq2 6738 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐴𝑦) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
104 fveq2 6738 . . . . . . . . . . . . . . . . . 18 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → (𝐵𝑦) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
105103, 104eqeq12d 2755 . . . . . . . . . . . . . . . . 17 (𝑦 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
106105rspccv 3549 . . . . . . . . . . . . . . . 16 (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
107106ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ( {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥 → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
108102, 107mtod 201 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥)
109 simpll 767 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 ∈ On)
110 oninton 7600 . . . . . . . . . . . . . . . . 17 (({𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ≠ ∅) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
11182, 83, 110sylancr 590 . . . . . . . . . . . . . . . 16 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
112111adantl 485 . . . . . . . . . . . . . . 15 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On)
113 ontri1 6267 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ On) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
114109, 112, 113syl2anc 587 . . . . . . . . . . . . . 14 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → (𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ↔ ¬ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ∈ 𝑥))
115108, 114mpbird 260 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
116 intss1 4890 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
117116adantl 485 . . . . . . . . . . . . 13 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)} ⊆ 𝑥)
118115, 117eqssd 3934 . . . . . . . . . . . 12 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ 𝑥 ∈ {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
11981, 118syldan 594 . . . . . . . . . . 11 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥) ≠ (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
12075, 119sylan2 596 . . . . . . . . . 10 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → 𝑥 = {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})
121120fveq2d 6742 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐴𝑥) = (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
122120fveq2d 6742 . . . . . . . . 9 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐵𝑥) = (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
123121, 122breq12d 5082 . . . . . . . 8 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
124123biimpd 232 . . . . . . 7 (((𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦)) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
125124ex 416 . . . . . 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 457 . . . 4 (𝑥 ∈ On → ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
128127rexlimiv 3209 . . 3 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) → (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}))
12950, 128impbid1 228 . 2 ((𝐴 No 𝐵 No ) → ((𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}) ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
1301, 129bitr4d 285 1 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ (𝐴 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵 {𝑎 ∈ On ∣ (𝐴𝑎) ≠ (𝐵𝑎)})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3o 1088   = wceq 1543  wcel 2112  wne 2943  wral 3064  wrex 3065  {crab 3068  Vcvv 3423  wss 3883  c0 4253  {ctp 4561  cop 4563   cint 4875   class class class wbr 5069  Oncon0 6233  suc csuc 6235  cfv 6400  1oc1o 8218  2oc2o 8219   No csur 33613   <s cslt 33614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5208  ax-nul 5215  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-pw 4531  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-int 4876  df-br 5070  df-opab 5132  df-tr 5178  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-ord 6236  df-on 6237  df-suc 6239  df-iota 6358  df-fv 6408  df-1o 8225  df-2o 8226  df-slt 33617
This theorem is referenced by:  sltintdifex  33634  sltres  33635  noextendlt  33642  noextendgt  33643  nosepnelem  33652  nosep1o  33654  nosep2o  33655  nosepdmlem  33656  nodenselem8  33664  nosupbnd2lem1  33688  noinfbnd2lem1  33703
  Copyright terms: Public domain W3C validator