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

Theorem nogt01o 27579
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 27559 . . . 4 <s Or No
2 simp11 1200 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → 𝐴 No )
3 sonr 5604 . . . 4 (( <s Or No 𝐴 No ) → ¬ 𝐴 <s 𝐴)
41, 2, 3sylancr 586 . . 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 27532 . . . . . . . 8 (𝐴 No → Fun 𝐴)
9 funrel 6558 . . . . . . . 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 484 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐴𝑋) = ∅)
14 nolt02olem 27577 . . . . . . 7 ((𝐴 No 𝑋 ∈ On ∧ (𝐴𝑋) = ∅) → dom 𝐴𝑋)
157, 12, 13, 14syl3anc 1368 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → dom 𝐴𝑋)
16 relssres 6015 . . . . . 6 ((Rel 𝐴 ∧ dom 𝐴𝑋) → (𝐴𝑋) = 𝐴)
1711, 15, 16syl2anc 583 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐴𝑋) = 𝐴)
18 simpl12 1246 . . . . . . 7 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐵 No )
19 nofun 27532 . . . . . . . 8 (𝐵 No → Fun 𝐵)
20 funrel 6558 . . . . . . . 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 27577 . . . . . . 7 ((𝐵 No 𝑋 ∈ On ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
2518, 12, 23, 24syl3anc 1368 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → dom 𝐵𝑋)
26 relssres 6015 . . . . . 6 ((Rel 𝐵 ∧ dom 𝐵𝑋) → (𝐵𝑋) = 𝐵)
2722, 25, 26syl2anc 583 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → (𝐵𝑋) = 𝐵)
286, 17, 273eqtr3d 2774 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐴 = 𝐵)
295, 28breqtrrd 5169 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = ∅) → 𝐴 <s 𝐴)
304, 29mtand 813 . 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 27530 . . . . . 6 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))))
342, 32, 33syl2anc 583 . . . . 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 3095 . . . . 5 (∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)) ↔ ¬ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
3736con2bii 357 . . . 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 8486 . . . . . . . . . . . 12 1o ≠ ∅
4039neii 2936 . . . . . . . . . . 11 ¬ 1o = ∅
41 eqtr2 2750 . . . . . . . . . . 11 ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) → 1o = ∅)
4240, 41mto 196 . . . . . . . . . 10 ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅)
43 df-2o 8465 . . . . . . . . . . . . 13 2o = suc 1o
44 2on 8478 . . . . . . . . . . . . . . . 16 2o ∈ On
4543, 44eqeltrri 2824 . . . . . . . . . . . . . . 15 suc 1o ∈ On
4645onordi 6468 . . . . . . . . . . . . . 14 Ord suc 1o
47 1oex 8474 . . . . . . . . . . . . . . 15 1o ∈ V
4847sucid 6439 . . . . . . . . . . . . . 14 1o ∈ suc 1o
49 nordeq 6376 . . . . . . . . . . . . . 14 ((Ord suc 1o ∧ 1o ∈ suc 1o) → suc 1o ≠ 1o)
5046, 48, 49mp2an 689 . . . . . . . . . . . . 13 suc 1o ≠ 1o
5143, 50eqnetri 3005 . . . . . . . . . . . 12 2o ≠ 1o
5251nesymi 2992 . . . . . . . . . . 11 ¬ 1o = 2o
53 eqtr2 2750 . . . . . . . . . . 11 ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) → 1o = 2o)
5452, 53mto 196 . . . . . . . . . 10 ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o)
55 2on0 8480 . . . . . . . . . . . 12 2o ≠ ∅
5655nesymi 2992 . . . . . . . . . . 11 ¬ ∅ = 2o
57 eqtr2 2750 . . . . . . . . . . 11 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o) → ∅ = 2o)
5856, 57mto 196 . . . . . . . . . 10 ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)
5942, 54, 583pm3.2i 1336 . . . . . . . . 9 (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o))
60 fvex 6897 . . . . . . . . . . . 12 ((𝐴𝑋)‘𝑥) ∈ V
6160, 60brtp 5516 . . . . . . . . . . 11 (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
62 3oran 1106 . . . . . . . . . . 11 (((((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
6361, 62bitri 275 . . . . . . . . . 10 (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1o ∧ ((𝐴𝑋)‘𝑥) = 2o) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2o)))
6463con2bii 357 . . . . . . . . 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 480 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = (𝐵𝑋))
6867fveq1d 6886 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋)‘𝑥) = ((𝐵𝑋)‘𝑥))
6968breq2d 5153 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐴𝑋)‘𝑥) ↔ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥)))
7065, 69mtbii 326 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥))
71 fvres 6903 . . . . . . . . 9 (𝑥𝑋 → ((𝐴𝑋)‘𝑥) = (𝐴𝑥))
72 fvres 6903 . . . . . . . . 9 (𝑥𝑋 → ((𝐵𝑋)‘𝑥) = (𝐵𝑥))
7371, 72breq12d 5154 . . . . . . . 8 (𝑥𝑋 → (((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥) ↔ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
7473notbid 318 . . . . . . 7 (𝑥𝑋 → (¬ ((𝐴𝑋)‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} ((𝐵𝑋)‘𝑥) ↔ ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
7570, 74syl5ibcom 244 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
7651neii 2936 . . . . . . . . . . 11 ¬ 2o = 1o
7776intnanr 487 . . . . . . . . . 10 ¬ (2o = 1o ∧ ∅ = ∅)
7856intnan 486 . . . . . . . . . 10 ¬ (2o = 1o ∧ ∅ = 2o)
7956intnan 486 . . . . . . . . . 10 ¬ (2o = ∅ ∧ ∅ = 2o)
8077, 78, 793pm3.2i 1336 . . . . . . . . 9 (¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬ (2o = 1o ∧ ∅ = 2o) ∧ ¬ (2o = ∅ ∧ ∅ = 2o))
81 2oex 8475 . . . . . . . . . . . 12 2o ∈ V
82 0ex 5300 . . . . . . . . . . . 12 ∅ ∈ V
8381, 82brtp 5516 . . . . . . . . . . 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 275 . . . . . . . . . 10 (2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅ ↔ ¬ (¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬ (2o = 1o ∧ ∅ = 2o) ∧ ¬ (2o = ∅ ∧ ∅ = 2o)))
8685con2bii 357 . . . . . . . . 9 ((¬ (2o = 1o ∧ ∅ = ∅) ∧ ¬ (2o = 1o ∧ ∅ = 2o) ∧ ¬ (2o = ∅ ∧ ∅ = 2o)) ↔ ¬ 2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅)
8780, 86mpbi 229 . . . . . . . 8 ¬ 2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅
88 simplr 766 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = 2o)
89 simpll3 1211 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐵𝑋) = ∅)
9088, 89breq12d 5154 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋) ↔ 2o{⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩}∅))
9187, 90mtbiri 327 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋))
92 fveq2 6884 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐴𝑥) = (𝐴𝑋))
93 fveq2 6884 . . . . . . . . 9 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
9492, 93breq12d 5154 . . . . . . . 8 (𝑥 = 𝑋 → ((𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥) ↔ (𝐴𝑋){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑋)))
9594notbid 318 . . . . . . 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 6884 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝐴𝑦) = (𝐴𝑋))
98 fveq2 6884 . . . . . . . . . . . . 13 (𝑦 = 𝑋 → (𝐵𝑦) = (𝐵𝑋))
9997, 98eqeq12d 2742 . . . . . . . . . . . 12 (𝑦 = 𝑋 → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴𝑋) = (𝐵𝑋)))
10099rspccv 3603 . . . . . . . . . . 11 (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → (𝑋𝑥 → (𝐴𝑋) = (𝐵𝑋)))
101100ad2antll 726 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑋𝑥 → (𝐴𝑋) = (𝐵𝑋)))
102 eqcom 2733 . . . . . . . . . 10 ((𝐴𝑋) = (𝐵𝑋) ↔ (𝐵𝑋) = (𝐴𝑋))
103101, 102imbitrdi 250 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑋𝑥 → (𝐵𝑋) = (𝐴𝑋)))
10489, 88eqeq12d 2742 . . . . . . . . 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 768 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥 ∈ On)
108 simpl13 1247 . . . . . . . . 9 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) → 𝑋 ∈ On)
109108adantr 480 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑋 ∈ On)
110 ontri1 6391 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
111 onsseleq 6398 . . . . . . . . 9 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
112110, 111bitr3d 281 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (¬ 𝑋𝑥 ↔ (𝑥𝑋𝑥 = 𝑋)))
113107, 109, 112syl2anc 583 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (¬ 𝑋𝑥 ↔ (𝑥𝑋𝑥 = 𝑋)))
114106, 113mpbid 231 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋𝑥 = 𝑋))
11575, 96, 114mpjaod 857 . . . . 5 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥))
116115expr 456 . . . 4 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) ∧ 𝑥 ∈ On) → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
117116ralrimiva 3140 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) ∧ (𝐴𝑋) = 2o) → ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵𝑥)))
11838, 117mtand 813 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐵𝑋) = ∅) → ¬ (𝐴𝑋) = 2o)
119 nofv 27540 . . . 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 395  wo 844  w3o 1083  w3a 1084   = wceq 1533  wcel 2098  wne 2934  wral 3055  wrex 3064  wss 3943  c0 4317  {ctp 4627  cop 4629   class class class wbr 5141   Or wor 5580  dom cdm 5669  cres 5671  Rel wrel 5674  Ord word 6356  Oncon0 6357  suc csuc 6359  Fun wfun 6530  cfv 6536  1oc1o 8457  2oc2o 8458   No csur 27523   <s cslt 27524
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-ord 6360  df-on 6361  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-1o 8464  df-2o 8465  df-no 27526  df-slt 27527
This theorem is referenced by:  noinfbnd1lem4  27609
  Copyright terms: Public domain W3C validator