Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  nolt02o Structured version   Visualization version   GIF version

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

Proof of Theorem nolt02o
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simp11 1111 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐴 No )
2 sltso 31952 . . . . . 6 <s Or No
3 sonr 5085 . . . . . 6 (( <s Or No 𝐴 No ) → ¬ 𝐴 <s 𝐴)
42, 3mpan 706 . . . . 5 (𝐴 No → ¬ 𝐴 <s 𝐴)
51, 4syl 17 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ 𝐴 <s 𝐴)
6 simp2r 1108 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐴 <s 𝐵)
7 breq2 4689 . . . . 5 (𝐴 = 𝐵 → (𝐴 <s 𝐴𝐴 <s 𝐵))
86, 7syl5ibrcom 237 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐴 = 𝐵𝐴 <s 𝐴))
95, 8mtod 189 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ 𝐴 = 𝐵)
10 simpl2l 1134 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = (𝐵𝑋))
11 simpl11 1156 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐴 No )
12 nofun 31927 . . . . . 6 (𝐴 No → Fun 𝐴)
13 funrel 5943 . . . . . 6 (Fun 𝐴 → Rel 𝐴)
1411, 12, 133syl 18 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → Rel 𝐴)
15 simpl13 1158 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝑋 ∈ On)
16 simpl3 1086 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = ∅)
17 nolt02olem 31969 . . . . . 6 ((𝐴 No 𝑋 ∈ On ∧ (𝐴𝑋) = ∅) → dom 𝐴𝑋)
1811, 15, 16, 17syl3anc 1366 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → dom 𝐴𝑋)
19 relssres 5472 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝑋) → (𝐴𝑋) = 𝐴)
2014, 18, 19syl2anc 694 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = 𝐴)
21 simpl12 1157 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐵 No )
22 nofun 31927 . . . . . 6 (𝐵 No → Fun 𝐵)
23 funrel 5943 . . . . . 6 (Fun 𝐵 → Rel 𝐵)
2421, 22, 233syl 18 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → Rel 𝐵)
25 simpr 476 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐵𝑋) = ∅)
26 nolt02olem 31969 . . . . . 6 ((𝐵 No 𝑋 ∈ On ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
2721, 15, 25, 26syl3anc 1366 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
28 relssres 5472 . . . . 5 ((Rel 𝐵 ∧ dom 𝐵𝑋) → (𝐵𝑋) = 𝐵)
2924, 27, 28syl2anc 694 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐵𝑋) = 𝐵)
3010, 20, 293eqtr3d 2693 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐴 = 𝐵)
319, 30mtand 692 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ (𝐵𝑋) = ∅)
32 simp12 1112 . . . . . 6 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐵 No )
33 sltval 31925 . . . . . 6 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
341, 32, 33syl2anc 694 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
356, 34mpbid 222 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
36 df-an 385 . . . . . 6 ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
3736rexbii 3070 . . . . 5 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ∃𝑥 ∈ On ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
38 rexnal 3024 . . . . 5 (∃𝑥 ∈ On ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
3937, 38bitri 264 . . . 4 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
4035, 39sylib 208 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
41 1on 7612 . . . . . . . . . . . . 13 1𝑜 ∈ On
4241elexi 3244 . . . . . . . . . . . 12 1𝑜 ∈ V
4342prid1 4329 . . . . . . . . . . 11 1𝑜 ∈ {1𝑜, 2𝑜}
4443nosgnn0i 31937 . . . . . . . . . 10 ∅ ≠ 1𝑜
4544neii 2825 . . . . . . . . 9 ¬ ∅ = 1𝑜
46 simpll3 1122 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = ∅)
47 simplr 807 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐵𝑋) = 1𝑜)
48 eqeq1 2655 . . . . . . . . . . . . 13 ((𝐴𝑋) = (𝐵𝑋) → ((𝐴𝑋) = ∅ ↔ (𝐵𝑋) = ∅))
4948anbi1d 741 . . . . . . . . . . . 12 ((𝐴𝑋) = (𝐵𝑋) → (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) ↔ ((𝐵𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜)))
50 eqtr2 2671 . . . . . . . . . . . 12 (((𝐵𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) → ∅ = 1𝑜)
5149, 50syl6bi 243 . . . . . . . . . . 11 ((𝐴𝑋) = (𝐵𝑋) → (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) → ∅ = 1𝑜))
5251com12 32 . . . . . . . . . 10 (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) → ((𝐴𝑋) = (𝐵𝑋) → ∅ = 1𝑜))
5346, 47, 52syl2anc 694 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋) = (𝐵𝑋) → ∅ = 1𝑜))
5445, 53mtoi 190 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋) = (𝐵𝑋))
55 simpr 476 . . . . . . . . 9 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → 𝑋𝑥)
56 simplrr 818 . . . . . . . . 9 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))
57 fveq2 6229 . . . . . . . . . . 11 (𝑦 = 𝑋 → (𝐴𝑦) = (𝐴𝑋))
58 fveq2 6229 . . . . . . . . . . 11 (𝑦 = 𝑋 → (𝐵𝑦) = (𝐵𝑋))
5957, 58eqeq12d 2666 . . . . . . . . . 10 (𝑦 = 𝑋 → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴𝑋) = (𝐵𝑋)))
6059rspcv 3336 . . . . . . . . 9 (𝑋𝑥 → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → (𝐴𝑋) = (𝐵𝑋)))
6155, 56, 60sylc 65 . . . . . . . 8 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → (𝐴𝑋) = (𝐵𝑋))
6254, 61mtand 692 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ 𝑋𝑥)
63 simprl 809 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥 ∈ On)
64 simpl13 1158 . . . . . . . . 9 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) → 𝑋 ∈ On)
6564adantr 480 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑋 ∈ On)
66 ontri1 5795 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
6763, 65, 66syl2anc 694 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
6862, 67mpbird 247 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥𝑋)
69 onsseleq 5803 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
7063, 65, 69syl2anc 694 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
71 eqtr2 2671 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 1𝑜) → ∅ = 1𝑜)
7271ancoms 468 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) → ∅ = 1𝑜)
7345, 72mto 188 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅)
74 df-1o 7605 . . . . . . . . . . . . . . . 16 1𝑜 = suc ∅
75 df-2o 7606 . . . . . . . . . . . . . . . 16 2𝑜 = suc 1𝑜
7674, 75eqeq12i 2665 . . . . . . . . . . . . . . 15 (1𝑜 = 2𝑜 ↔ suc ∅ = suc 1𝑜)
77 0elon 5816 . . . . . . . . . . . . . . . 16 ∅ ∈ On
78 suc11 5869 . . . . . . . . . . . . . . . 16 ((∅ ∈ On ∧ 1𝑜 ∈ On) → (suc ∅ = suc 1𝑜 ↔ ∅ = 1𝑜))
7977, 41, 78mp2an 708 . . . . . . . . . . . . . . 15 (suc ∅ = suc 1𝑜 ↔ ∅ = 1𝑜)
8076, 79bitri 264 . . . . . . . . . . . . . 14 (1𝑜 = 2𝑜 ↔ ∅ = 1𝑜)
8144, 80nemtbir 2918 . . . . . . . . . . . . 13 ¬ 1𝑜 = 2𝑜
82 eqtr2 2671 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) → 1𝑜 = 2𝑜)
8381, 82mto 188 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)
84 2on 7613 . . . . . . . . . . . . . . . . 17 2𝑜 ∈ On
8584elexi 3244 . . . . . . . . . . . . . . . 16 2𝑜 ∈ V
8685prid2 4330 . . . . . . . . . . . . . . 15 2𝑜 ∈ {1𝑜, 2𝑜}
8786nosgnn0i 31937 . . . . . . . . . . . . . 14 ∅ ≠ 2𝑜
8887neii 2825 . . . . . . . . . . . . 13 ¬ ∅ = 2𝑜
89 eqtr2 2671 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) → ∅ = 2𝑜)
9088, 89mto 188 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)
9173, 83, 903pm3.2i 1259 . . . . . . . . . . 11 (¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜))
92 fvex 6239 . . . . . . . . . . . . . 14 ((𝐴𝑋)‘𝑥) ∈ V
9392, 92brtp 31765 . . . . . . . . . . . . 13 (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥) ↔ ((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)))
94 3oran 1077 . . . . . . . . . . . . 13 (((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)))
9593, 94bitri 264 . . . . . . . . . . . 12 (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)))
9695con2bii 346 . . . . . . . . . . 11 ((¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)) ↔ ¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥))
9791, 96mpbi 220 . . . . . . . . . 10 ¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥)
98 simpl2l 1134 . . . . . . . . . . . . 13 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) → (𝐴𝑋) = (𝐵𝑋))
9998adantr 480 . . . . . . . . . . . 12 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = (𝐵𝑋))
10099fveq1d 6231 . . . . . . . . . . 11 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋)‘𝑥) = ((𝐵𝑋)‘𝑥))
101100breq2d 4697 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥) ↔ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥)))
10297, 101mtbii 315 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥))
103 fvres 6245 . . . . . . . . . . 11 (𝑥𝑋 → ((𝐴𝑋)‘𝑥) = (𝐴𝑥))
104 fvres 6245 . . . . . . . . . . 11 (𝑥𝑋 → ((𝐵𝑋)‘𝑥) = (𝐵𝑥))
105103, 104breq12d 4698 . . . . . . . . . 10 (𝑥𝑋 → (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥) ↔ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
106105notbid 307 . . . . . . . . 9 (𝑥𝑋 → (¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥) ↔ ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
107102, 106syl5ibcom 235 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
10845intnanr 981 . . . . . . . . . . . 12 ¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅)
10945intnanr 981 . . . . . . . . . . . 12 ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜)
11081intnan 980 . . . . . . . . . . . 12 ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)
111108, 109, 1103pm3.2i 1259 . . . . . . . . . . 11 (¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜))
112 0ex 4823 . . . . . . . . . . . . . 14 ∅ ∈ V
113112, 42brtp 31765 . . . . . . . . . . . . 13 (∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜 ↔ ((∅ = 1𝑜 ∧ 1𝑜 = ∅) ∨ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∨ (∅ = ∅ ∧ 1𝑜 = 2𝑜)))
114 3oran 1077 . . . . . . . . . . . . 13 (((∅ = 1𝑜 ∧ 1𝑜 = ∅) ∨ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∨ (∅ = ∅ ∧ 1𝑜 = 2𝑜)) ↔ ¬ (¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)))
115113, 114bitri 264 . . . . . . . . . . . 12 (∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜 ↔ ¬ (¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)))
116115con2bii 346 . . . . . . . . . . 11 ((¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)) ↔ ¬ ∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜)
117111, 116mpbi 220 . . . . . . . . . 10 ¬ ∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜
11846, 47breq12d 4698 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋) ↔ ∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜))
119117, 118mtbiri 316 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋))
120 fveq2 6229 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝐴𝑥) = (𝐴𝑋))
121 fveq2 6229 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
122120, 121breq12d 4698 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋)))
123122notbid 307 . . . . . . . . 9 (𝑥 = 𝑋 → (¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ ¬ (𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋)))
124119, 123syl5ibrcom 237 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
125107, 124jaod 394 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝑥𝑋𝑥 = 𝑋) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
12670, 125sylbid 230 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
12768, 126mpd 15 . . . . 5 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))
128127expr 642 . . . 4 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ 𝑥 ∈ On) → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
129128ralrimiva 2995 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) → ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
13040, 129mtand 692 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ (𝐵𝑋) = 1𝑜)
131 nofv 31935 . . . 4 (𝐵 No → ((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜))
13232, 131syl 17 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜))
133 3orrot 1061 . . . 4 (((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜) ↔ ((𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅))
134 3orrot 1061 . . . 4 (((𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅) ↔ ((𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜))
135133, 134bitri 264 . . 3 (((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜) ↔ ((𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜))
136132, 135sylib 208 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ((𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜))
13731, 130, 136ecase23d 1476 1 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐵𝑋) = 2𝑜)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3o 1053  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wrex 2942  wss 3607  c0 3948  {ctp 4214  cop 4216   class class class wbr 4685   Or wor 5063  dom cdm 5143  cres 5145  Rel wrel 5148  Oncon0 5761  suc csuc 5763  Fun wfun 5920  cfv 5926  1𝑜c1o 7598  2𝑜c2o 7599   No csur 31918   <s cslt 31919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-ord 5764  df-on 5765  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-1o 7605  df-2o 7606  df-no 31921  df-slt 31922
This theorem is referenced by:  nosupbnd1lem4  31982
  Copyright terms: Public domain W3C validator