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

Theorem nogt01o 27649
Description: Given 𝐴 greater than 𝐵, equal to 𝐵 up to 𝑋, and 𝐵(𝑋) undefined, then 𝐴(𝑋) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.)
Assertion
Ref Expression
nogt01o (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = 1o)

Proof of Theorem nogt01o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sltso 27629 . . . 4 <s Or No
2 simp11 1200 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → 𝐴 No )
3 sonr 5617 . . . 4 (( <s Or No 𝐴 No ) → ¬ 𝐴 <s 𝐴)
41, 2, 3sylancr 585 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ¬ 𝐴 <s 𝐴)
5 simpl2r 1224 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐴 <s 𝐵)
6 simpl2l 1223 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐴𝑋) = (𝐵𝑋))
7 simpl11 1245 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐴 No )
8 nofun 27602 . . . . . . . 8 (𝐴 No → Fun 𝐴)
9 funrel 6575 . . . . . . . 8 (Fun 𝐴 → Rel 𝐴)
108, 9syl 17 . . . . . . 7 (𝐴 No → Rel 𝐴)
117, 10syl 17 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → Rel 𝐴)
12 simpl13 1247 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝑋 ∈ On)
13 simpr 483 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐴𝑋) = ∅)
14 nolt02olem 27647 . . . . . . 7 ((𝐴 No 𝑋 ∈ On ∧ (𝐴𝑋) = ∅) → dom 𝐴𝑋)
157, 12, 13, 14syl3anc 1368 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → dom 𝐴𝑋)
16 relssres 6031 . . . . . 6 ((Rel 𝐴 ∧ dom 𝐴𝑋) → (𝐴𝑋) = 𝐴)
1711, 15, 16syl2anc 582 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐴𝑋) = 𝐴)
18 simpl12 1246 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐵 No )
19 nofun 27602 . . . . . . . 8 (𝐵 No → Fun 𝐵)
20 funrel 6575 . . . . . . . 8 (Fun 𝐵 → Rel 𝐵)
2119, 20syl 17 . . . . . . 7 (𝐵 No → Rel 𝐵)
2218, 21syl 17 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → Rel 𝐵)
23 simpl3 1190 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐵𝑋) = ∅)
24 nolt02olem 27647 . . . . . . 7 ((𝐵 No 𝑋 ∈ On ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
2518, 12, 23, 24syl3anc 1368 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → dom 𝐵𝑋)
26 relssres 6031 . . . . . 6 ((Rel 𝐵 ∧ dom 𝐵𝑋) → (𝐵𝑋) = 𝐵)
2722, 25, 26syl2anc 582 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐵𝑋) = 𝐵)
286, 17, 273eqtr3d 2776 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐴 = 𝐵)
295, 28breqtrrd 5180 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐴 <s 𝐴)
304, 29mtand 814 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ¬ (𝐴𝑋) = ∅)
31 simp2r 1197 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → 𝐴 <s 𝐵)
32 simp12 1201 . . . . . 6 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → 𝐵 No )
33 sltval 27600 . . . . . 6 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
342, 32, 33syl2anc 582 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
3531, 34mpbid 231 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
36 ralinexa 3098 . . . . 5 (∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
3736con2bii 356 . . . 4 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
3835, 37sylib 217 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
39 1n0 8515 . . . . . . . . . . . 12 1o ≠ ∅
4039neii 2939 . . . . . . . . . . 11 ¬ 1o = ∅
41 eqtr2 2752 . . . . . . . . . . 11 ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) → 1o = ∅)
4240, 41mto 196 . . . . . . . . . 10 ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅)
43 df-2o 8494 . . . . . . . . . . . . 13 2o = suc 1o
44 2on 8507 . . . . . . . . . . . . . . . 16 2o ∈ On
4543, 44eqeltrri 2826 . . . . . . . . . . . . . . 15 suc 1o ∈ On
4645onordi 6485 . . . . . . . . . . . . . 14 Ord suc 1o
47 1oex 8503 . . . . . . . . . . . . . . 15 1o ∈ V
4847sucid 6456 . . . . . . . . . . . . . 14 1o ∈ suc 1o
49 nordeq 6393 . . . . . . . . . . . . . 14 ((Ord suc 1o ∧ 1o ∈ suc 1o) → suc 1o ≠ 1o)
5046, 48, 49mp2an 690 . . . . . . . . . . . . 13 suc 1o ≠ 1o
5143, 50eqnetri 3008 . . . . . . . . . . . 12 2o ≠ 1o
5251nesymi 2995 . . . . . . . . . . 11 ¬ 1o = 2o
53 eqtr2 2752 . . . . . . . . . . 11 ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) → 1o = 2o)
5452, 53mto 196 . . . . . . . . . 10 ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o)
55 2on0 8509 . . . . . . . . . . . 12 2o ≠ ∅
5655nesymi 2995 . . . . . . . . . . 11 ¬ ∅ = 2o
57 eqtr2 2752 . . . . . . . . . . 11 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o) → ∅ = 2o)
5856, 57mto 196 . . . . . . . . . 10 ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)
5942, 54, 583pm3.2i 1336 . . . . . . . . 9 (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o))
60 fvex 6915 . . . . . . . . . . . 12 ((𝐴𝑋)‘𝑥) ∈ V
6160, 60brtp 5529 . . . . . . . . . . 11 (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
62 3oran 1106 . . . . . . . . . . 11 (((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
6361, 62bitri 274 . . . . . . . . . 10 (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
6463con2bii 356 . . . . . . . . 9 ((¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)) ↔ ¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥))
6559, 64mpbi 229 . . . . . . . 8 ¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥)
66 simpl2l 1223 . . . . . . . . . . 11 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) → (𝐴𝑋) = (𝐵𝑋))
6766adantr 479 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = (𝐵𝑋))
6867fveq1d 6904 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋)‘𝑥) = ((𝐵𝑋)‘𝑥))
6968breq2d 5164 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥)))
7065, 69mtbii 325 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥))
71 fvres 6921 . . . . . . . . 9 (𝑥𝑋 → ((𝐴𝑋)‘𝑥) = (𝐴𝑥))
72 fvres 6921 . . . . . . . . 9 (𝑥𝑋 → ((𝐵𝑋)‘𝑥) = (𝐵𝑥))
7371, 72breq12d 5165 . . . . . . . 8 (𝑥𝑋 → (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥) ↔ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
7473notbid 317 . . . . . . 7 (𝑥𝑋 → (¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥) ↔ ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
7570, 74syl5ibcom 244 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
7651neii 2939 . . . . . . . . . . 11 ¬ 2o = 1o
7776intnanr 486 . . . . . . . . . 10 ¬ (2o = 1o ∧ ∅ = ∅)
7856intnan 485 . . . . . . . . . 10 ¬ (2o = 1o ∧ ∅ = 2o)
7956intnan 485 . . . . . . . . . 10 ¬ (2o = ∅ ∧ ∅ = 2o)
8077, 78, 793pm3.2i 1336 . . . . . . . . 9 (¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬ (2o = 1o ∧ ∅ = 2o) ∧ ¬ (2o = ∅ ∧ ∅ = 2o))
81 2oex 8504 . . . . . . . . . . . 12 2o ∈ V
82 0ex 5311 . . . . . . . . . . . 12 ∅ ∈ V
8381, 82brtp 5529 . . . . . . . . . . 11 (2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅ ↔ ((2o = 1o ∧ ∅ = ∅) ∨ (2o = 1o ∧ ∅ = 2o) ∨ (2o = ∅ ∧ ∅ = 2o)))
84 3oran 1106 . . . . . . . . . . 11 (((2o = 1o ∧ ∅ = ∅) ∨ (2o = 1o ∧ ∅ = 2o) ∨ (2o = ∅ ∧ ∅ = 2o)) ↔ ¬ (¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬ (2o = 1o ∧ ∅ = 2o) ∧ ¬ (2o = ∅ ∧ ∅ = 2o)))
8583, 84bitri 274 . . . . . . . . . 10 (2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅ ↔ ¬ (¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬ (2o = 1o ∧ ∅ = 2o) ∧ ¬ (2o = ∅ ∧ ∅ = 2o)))
8685con2bii 356 . . . . . . . . 9 ((¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬ (2o = 1o ∧ ∅ = 2o) ∧ ¬ (2o = ∅ ∧ ∅ = 2o)) ↔ ¬ 2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅)
8780, 86mpbi 229 . . . . . . . 8 ¬ 2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅
88 simplr 767 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = 2o)
89 simpll3 1211 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐵𝑋) = ∅)
9088, 89breq12d 5165 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋) ↔ 2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅))
9187, 90mtbiri 326 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋))
92 fveq2 6902 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐴𝑥) = (𝐴𝑋))
93 fveq2 6902 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
9492, 93breq12d 5165 . . . . . . . 8 (𝑥 = 𝑋 → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋)))
9594notbid 317 . . . . . . 7 (𝑥 = 𝑋 → (¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ ¬ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋)))
9691, 95syl5ibrcom 246 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
97 fveq2 6902 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝐴𝑦) = (𝐴𝑋))
98 fveq2 6902 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝐵𝑦) = (𝐵𝑋))
9997, 98eqeq12d 2744 . . . . . . . . . . . 12 (𝑦 = 𝑋 → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴𝑋) = (𝐵𝑋)))
10099rspccv 3608 . . . . . . . . . . 11 (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → (𝑋𝑥 → (𝐴𝑋) = (𝐵𝑋)))
101100ad2antll 727 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑋𝑥 → (𝐴𝑋) = (𝐵𝑋)))
102 eqcom 2735 . . . . . . . . . 10 ((𝐴𝑋) = (𝐵𝑋) ↔ (𝐵𝑋) = (𝐴𝑋))
103101, 102imbitrdi 250 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑋𝑥 → (𝐵𝑋) = (𝐴𝑋)))
10489, 88eqeq12d 2744 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐵𝑋) = (𝐴𝑋) ↔ ∅ = 2o))
105103, 104sylibd 238 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑋𝑥 → ∅ = 2o))
10656, 105mtoi 198 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ 𝑋𝑥)
107 simprl 769 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥 ∈ On)
108 simpl13 1247 . . . . . . . . 9 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) → 𝑋 ∈ On)
109108adantr 479 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑋 ∈ On)
110 ontri1 6408 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
111 onsseleq 6415 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
112110, 111bitr3d 280 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (¬ 𝑋𝑥 ↔ (𝑥𝑋𝑥 = 𝑋)))
113107, 109, 112syl2anc 582 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (¬ 𝑋𝑥 ↔ (𝑥𝑋𝑥 = 𝑋)))
114106, 113mpbid 231 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋𝑥 = 𝑋))
11575, 96, 114mpjaod 858 . . . . 5 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))
116115expr 455 . . . 4 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ 𝑥 ∈ On) → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
117116ralrimiva 3143 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) → ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
11838, 117mtand 814 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ¬ (𝐴𝑋) = 2o)
119 nofv 27610 . . . 4 (𝐴 No → ((𝐴𝑋) = ∅ ∨ (𝐴𝑋) = 1o ∨ (𝐴𝑋) = 2o))
1202, 119syl 17 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ((𝐴𝑋) = ∅ ∨ (𝐴𝑋) = 1o ∨ (𝐴𝑋) = 2o))
121 3orcoma 1090 . . 3 (((𝐴𝑋) = ∅ ∨ (𝐴𝑋) = 1o ∨ (𝐴𝑋) = 2o) ↔ ((𝐴𝑋) = 1o ∨ (𝐴𝑋) = ∅ ∨ (𝐴𝑋) = 2o))
122120, 121sylib 217 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ((𝐴𝑋) = 1o ∨ (𝐴𝑋) = ∅ ∨ (𝐴𝑋) = 2o))
12330, 118, 122ecase23d 1469 1 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = 1o)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845  w3o 1083  w3a 1084   = wceq 1533  wcel 2098  wne 2937  wral 3058  wrex 3067  wss 3949  c0 4326  {ctp 4636  cop 4638   class class class wbr 5152   Or wor 5593  dom cdm 5682  cres 5684  Rel wrel 5687  Ord word 6373  Oncon0 6374  suc csuc 6376  Fun wfun 6547  cfv 6553  1oc1o 8486  2oc2o 8487   No csur 27593   <s cslt 27594
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6377  df-on 6378  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-1o 8493  df-2o 8494  df-no 27596  df-slt 27597
This theorem is referenced by:  noinfbnd1lem4  27679
  Copyright terms: Public domain W3C validator