MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nolt02o Structured version   Visualization version   GIF version

Theorem nolt02o 27740
Description: Given 𝐴 less-than 𝐵, equal to 𝐵 up to 𝑋, and undefined at 𝑋, then 𝐵(𝑋) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.)
Assertion
Ref Expression
nolt02o (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐵𝑋) = 2o)

Proof of Theorem nolt02o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp11 1204 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐴 No )
2 sltso 27721 . . . . . 6 <s Or No
3 sonr 5616 . . . . . 6 (( <s Or No 𝐴 No ) → ¬ 𝐴 <s 𝐴)
42, 3mpan 690 . . . . 5 (𝐴 No → ¬ 𝐴 <s 𝐴)
51, 4syl 17 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ 𝐴 <s 𝐴)
6 simp2r 1201 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐴 <s 𝐵)
7 breq2 5147 . . . . 5 (𝐴 = 𝐵 → (𝐴 <s 𝐴𝐴 <s 𝐵))
86, 7syl5ibrcom 247 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐴 = 𝐵𝐴 <s 𝐴))
95, 8mtod 198 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ 𝐴 = 𝐵)
10 simpl2l 1227 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = (𝐵𝑋))
11 simpl11 1249 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐴 No )
12 nofun 27694 . . . . . 6 (𝐴 No → Fun 𝐴)
13 funrel 6583 . . . . . 6 (Fun 𝐴 → Rel 𝐴)
1411, 12, 133syl 18 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → Rel 𝐴)
15 simpl13 1251 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝑋 ∈ On)
16 simpl3 1194 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = ∅)
17 nolt02olem 27739 . . . . . 6 ((𝐴 No 𝑋 ∈ On ∧ (𝐴𝑋) = ∅) → dom 𝐴𝑋)
1811, 15, 16, 17syl3anc 1373 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → dom 𝐴𝑋)
19 relssres 6040 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝑋) → (𝐴𝑋) = 𝐴)
2014, 18, 19syl2anc 584 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = 𝐴)
21 simpl12 1250 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐵 No )
22 nofun 27694 . . . . . 6 (𝐵 No → Fun 𝐵)
23 funrel 6583 . . . . . 6 (Fun 𝐵 → Rel 𝐵)
2421, 22, 233syl 18 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → Rel 𝐵)
25 simpr 484 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐵𝑋) = ∅)
26 nolt02olem 27739 . . . . . 6 ((𝐵 No 𝑋 ∈ On ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
2721, 15, 25, 26syl3anc 1373 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
28 relssres 6040 . . . . 5 ((Rel 𝐵 ∧ dom 𝐵𝑋) → (𝐵𝑋) = 𝐵)
2924, 27, 28syl2anc 584 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐵𝑋) = 𝐵)
3010, 20, 293eqtr3d 2785 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐴 = 𝐵)
319, 30mtand 816 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ (𝐵𝑋) = ∅)
32 simp12 1205 . . . . . 6 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐵 No )
33 sltval 27692 . . . . . 6 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
341, 32, 33syl2anc 584 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
356, 34mpbid 232 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
36 df-an 396 . . . . . 6 ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
3736rexbii 3094 . . . . 5 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ ∃𝑥 ∈ On ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
38 rexnal 3100 . . . . 5 (∃𝑥 ∈ On ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
3937, 38bitri 275 . . . 4 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
4035, 39sylib 218 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
41 1oex 8516 . . . . . . . . . . . 12 1o ∈ V
4241prid1 4762 . . . . . . . . . . 11 1o ∈ {1o, 2o}
4342nosgnn0i 27704 . . . . . . . . . 10 ∅ ≠ 1o
4443neii 2942 . . . . . . . . 9 ¬ ∅ = 1o
45 simpll3 1215 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = ∅)
46 simplr 769 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐵𝑋) = 1o)
47 eqeq1 2741 . . . . . . . . . . . . 13 ((𝐴𝑋) = (𝐵𝑋) → ((𝐴𝑋) = ∅ ↔ (𝐵𝑋) = ∅))
4847anbi1d 631 . . . . . . . . . . . 12 ((𝐴𝑋) = (𝐵𝑋) → (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1o) ↔ ((𝐵𝑋) = ∅ ∧ (𝐵𝑋) = 1o)))
49 eqtr2 2761 . . . . . . . . . . . 12 (((𝐵𝑋) = ∅ ∧ (𝐵𝑋) = 1o) → ∅ = 1o)
5048, 49biimtrdi 253 . . . . . . . . . . 11 ((𝐴𝑋) = (𝐵𝑋) → (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1o) → ∅ = 1o))
5150com12 32 . . . . . . . . . 10 (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1o) → ((𝐴𝑋) = (𝐵𝑋) → ∅ = 1o))
5245, 46, 51syl2anc 584 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋) = (𝐵𝑋) → ∅ = 1o))
5344, 52mtoi 199 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋) = (𝐵𝑋))
54 simpr 484 . . . . . . . . 9 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → 𝑋𝑥)
55 simplrr 778 . . . . . . . . 9 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))
56 fveq2 6906 . . . . . . . . . . 11 (𝑦 = 𝑋 → (𝐴𝑦) = (𝐴𝑋))
57 fveq2 6906 . . . . . . . . . . 11 (𝑦 = 𝑋 → (𝐵𝑦) = (𝐵𝑋))
5856, 57eqeq12d 2753 . . . . . . . . . 10 (𝑦 = 𝑋 → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴𝑋) = (𝐵𝑋)))
5958rspcv 3618 . . . . . . . . 9 (𝑋𝑥 → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → (𝐴𝑋) = (𝐵𝑋)))
6054, 55, 59sylc 65 . . . . . . . 8 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → (𝐴𝑋) = (𝐵𝑋))
6153, 60mtand 816 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ 𝑋𝑥)
62 simprl 771 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥 ∈ On)
63 simpl13 1251 . . . . . . . . 9 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) → 𝑋 ∈ On)
6463adantr 480 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑋 ∈ On)
65 ontri1 6418 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
6662, 64, 65syl2anc 584 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
6761, 66mpbird 257 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥𝑋)
68 onsseleq 6425 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
6962, 64, 68syl2anc 584 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
70 eqtr2 2761 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 1o) → ∅ = 1o)
7170ancoms 458 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) → ∅ = 1o)
7244, 71mto 197 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅)
73 df-1o 8506 . . . . . . . . . . . . . . . 16 1o = suc ∅
74 df-2o 8507 . . . . . . . . . . . . . . . 16 2o = suc 1o
7573, 74eqeq12i 2755 . . . . . . . . . . . . . . 15 (1o = 2o ↔ suc ∅ = suc 1o)
76 0elon 6438 . . . . . . . . . . . . . . . 16 ∅ ∈ On
77 1on 8518 . . . . . . . . . . . . . . . 16 1o ∈ On
78 suc11 6491 . . . . . . . . . . . . . . . 16 ((∅ ∈ On ∧ 1o ∈ On) → (suc ∅ = suc 1o ↔ ∅ = 1o))
7976, 77, 78mp2an 692 . . . . . . . . . . . . . . 15 (suc ∅ = suc 1o ↔ ∅ = 1o)
8075, 79bitri 275 . . . . . . . . . . . . . 14 (1o = 2o ↔ ∅ = 1o)
8143, 80nemtbir 3038 . . . . . . . . . . . . 13 ¬ 1o = 2o
82 eqtr2 2761 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) → 1o = 2o)
8381, 82mto 197 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o)
84 2on 8520 . . . . . . . . . . . . . . . . 17 2o ∈ On
8584elexi 3503 . . . . . . . . . . . . . . . 16 2o ∈ V
8685prid2 4763 . . . . . . . . . . . . . . 15 2o ∈ {1o, 2o}
8786nosgnn0i 27704 . . . . . . . . . . . . . 14 ∅ ≠ 2o
8887neii 2942 . . . . . . . . . . . . 13 ¬ ∅ = 2o
89 eqtr2 2761 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o) → ∅ = 2o)
9088, 89mto 197 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)
9172, 83, 903pm3.2i 1340 . . . . . . . . . . 11 (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o))
92 fvex 6919 . . . . . . . . . . . . . 14 ((𝐴𝑋)‘𝑥) ∈ V
9392, 92brtp 5528 . . . . . . . . . . . . 13 (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
94 3oran 1109 . . . . . . . . . . . . 13 (((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
9593, 94bitri 275 . . . . . . . . . . . 12 (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
9695con2bii 357 . . . . . . . . . . 11 ((¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)) ↔ ¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥))
9791, 96mpbi 230 . . . . . . . . . 10 ¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥)
98 simpl2l 1227 . . . . . . . . . . . . 13 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) → (𝐴𝑋) = (𝐵𝑋))
9998adantr 480 . . . . . . . . . . . 12 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = (𝐵𝑋))
10099fveq1d 6908 . . . . . . . . . . 11 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋)‘𝑥) = ((𝐵𝑋)‘𝑥))
101100breq2d 5155 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥)))
10297, 101mtbii 326 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥))
103 fvres 6925 . . . . . . . . . . 11 (𝑥𝑋 → ((𝐴𝑋)‘𝑥) = (𝐴𝑥))
104 fvres 6925 . . . . . . . . . . 11 (𝑥𝑋 → ((𝐵𝑋)‘𝑥) = (𝐵𝑥))
105103, 104breq12d 5156 . . . . . . . . . 10 (𝑥𝑋 → (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥) ↔ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
106105notbid 318 . . . . . . . . 9 (𝑥𝑋 → (¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥) ↔ ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
107102, 106syl5ibcom 245 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
10844intnanr 487 . . . . . . . . . . . 12 ¬ (∅ = 1o ∧ 1o = ∅)
10944intnanr 487 . . . . . . . . . . . 12 ¬ (∅ = 1o ∧ 1o = 2o)
11081intnan 486 . . . . . . . . . . . 12 ¬ (∅ = ∅ ∧ 1o = 2o)
111108, 109, 1103pm3.2i 1340 . . . . . . . . . . 11 (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o))
112 0ex 5307 . . . . . . . . . . . . . 14 ∅ ∈ V
113112, 41brtp 5528 . . . . . . . . . . . . 13 (∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o ↔ ((∅ = 1o ∧ 1o = ∅) ∨ (∅ = 1o ∧ 1o = 2o) ∨ (∅ = ∅ ∧ 1o = 2o)))
114 3oran 1109 . . . . . . . . . . . . 13 (((∅ = 1o ∧ 1o = ∅) ∨ (∅ = 1o ∧ 1o = 2o) ∨ (∅ = ∅ ∧ 1o = 2o)) ↔ ¬ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)))
115113, 114bitri 275 . . . . . . . . . . . 12 (∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o ↔ ¬ (¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)))
116115con2bii 357 . . . . . . . . . . 11 ((¬ (∅ = 1o ∧ 1o = ∅) ∧ ¬ (∅ = 1o ∧ 1o = 2o) ∧ ¬ (∅ = ∅ ∧ 1o = 2o)) ↔ ¬ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o)
117111, 116mpbi 230 . . . . . . . . . 10 ¬ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o
11845, 46breq12d 5156 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋) ↔ ∅{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}1o))
119117, 118mtbiri 327 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋))
120 fveq2 6906 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝐴𝑥) = (𝐴𝑋))
121 fveq2 6906 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
122120, 121breq12d 5156 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋)))
123122notbid 318 . . . . . . . . 9 (𝑥 = 𝑋 → (¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ ¬ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋)))
124119, 123syl5ibrcom 247 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
125107, 124jaod 860 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝑥𝑋𝑥 = 𝑋) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
12669, 125sylbid 240 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
12767, 126mpd 15 . . . . 5 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))
128127expr 456 . . . 4 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) ∧ 𝑥 ∈ On) → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
129128ralrimiva 3146 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1o) → ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
13040, 129mtand 816 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ (𝐵𝑋) = 1o)
131 nofv 27702 . . . 4 (𝐵 No → ((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1o ∨ (𝐵𝑋) = 2o))
13232, 131syl 17 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1o ∨ (𝐵𝑋) = 2o))
133 3orrot 1092 . . . 4 (((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1o ∨ (𝐵𝑋) = 2o) ↔ ((𝐵𝑋) = 1o ∨ (𝐵𝑋) = 2o ∨ (𝐵𝑋) = ∅))
134 3orrot 1092 . . . 4 (((𝐵𝑋) = 1o ∨ (𝐵𝑋) = 2o ∨ (𝐵𝑋) = ∅) ↔ ((𝐵𝑋) = 2o ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1o))
135133, 134bitri 275 . . 3 (((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1o ∨ (𝐵𝑋) = 2o) ↔ ((𝐵𝑋) = 2o ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1o))
136132, 135sylib 218 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ((𝐵𝑋) = 2o ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1o))
13731, 130, 136ecase23d 1475 1 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐵𝑋) = 2o)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3o 1086  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  wss 3951  c0 4333  {ctp 4630  cop 4632   class class class wbr 5143   Or wor 5591  dom cdm 5685  cres 5687  Rel wrel 5690  Oncon0 6384  suc csuc 6386  Fun wfun 6555  cfv 6561  1oc1o 8499  2oc2o 8500   No csur 27684   <s cslt 27685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-1o 8506  df-2o 8507  df-no 27687  df-slt 27688
This theorem is referenced by:  nosupbnd1lem4  27756
  Copyright terms: Public domain W3C validator