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 32171
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 1253 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐴 No )
2 sltso 32153 . . . . . 6 <s Or No
3 sonr 5260 . . . . . 6 (( <s Or No 𝐴 No ) → ¬ 𝐴 <s 𝐴)
42, 3mpan 673 . . . . 5 (𝐴 No → ¬ 𝐴 <s 𝐴)
51, 4syl 17 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ 𝐴 <s 𝐴)
6 simp2r 1250 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐴 <s 𝐵)
7 breq2 4855 . . . . 5 (𝐴 = 𝐵 → (𝐴 <s 𝐴𝐴 <s 𝐵))
86, 7syl5ibrcom 238 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐴 = 𝐵𝐴 <s 𝐴))
95, 8mtod 189 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ 𝐴 = 𝐵)
10 simpl2l 1290 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = (𝐵𝑋))
11 simpl11 1322 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐴 No )
12 nofun 32128 . . . . . 6 (𝐴 No → Fun 𝐴)
13 funrel 6121 . . . . . 6 (Fun 𝐴 → Rel 𝐴)
1411, 12, 133syl 18 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → Rel 𝐴)
15 simpl13 1326 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝑋 ∈ On)
16 simpl3 1239 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = ∅)
17 nolt02olem 32170 . . . . . 6 ((𝐴 No 𝑋 ∈ On ∧ (𝐴𝑋) = ∅) → dom 𝐴𝑋)
1811, 15, 16, 17syl3anc 1483 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → dom 𝐴𝑋)
19 relssres 5648 . . . . 5 ((Rel 𝐴 ∧ dom 𝐴𝑋) → (𝐴𝑋) = 𝐴)
2014, 18, 19syl2anc 575 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐴𝑋) = 𝐴)
21 simpl12 1324 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐵 No )
22 nofun 32128 . . . . . 6 (𝐵 No → Fun 𝐵)
23 funrel 6121 . . . . . 6 (Fun 𝐵 → Rel 𝐵)
2421, 22, 233syl 18 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → Rel 𝐵)
25 simpr 473 . . . . . 6 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐵𝑋) = ∅)
26 nolt02olem 32170 . . . . . 6 ((𝐵 No 𝑋 ∈ On ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
2721, 15, 25, 26syl3anc 1483 . . . . 5 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → dom 𝐵𝑋)
28 relssres 5648 . . . . 5 ((Rel 𝐵 ∧ dom 𝐵𝑋) → (𝐵𝑋) = 𝐵)
2924, 27, 28syl2anc 575 . . . 4 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → (𝐵𝑋) = 𝐵)
3010, 20, 293eqtr3d 2855 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = ∅) → 𝐴 = 𝐵)
319, 30mtand 841 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ (𝐵𝑋) = ∅)
32 simp12 1254 . . . . . 6 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → 𝐵 No )
33 sltval 32126 . . . . . 6 ((𝐴 No 𝐵 No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
341, 32, 33syl2anc 575 . . . . 5 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))))
356, 34mpbid 223 . . . 4 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
36 df-an 385 . . . . . 6 ((∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
3736rexbii 3236 . . . . 5 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ∃𝑥 ∈ On ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
38 rexnal 3189 . . . . 5 (∃𝑥 ∈ On ¬ (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
3937, 38bitri 266 . . . 4 (∃𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) ∧ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)) ↔ ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
4035, 39sylib 209 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
41 1oex 7807 . . . . . . . . . . . 12 1𝑜 ∈ V
4241prid1 4495 . . . . . . . . . . 11 1𝑜 ∈ {1𝑜, 2𝑜}
4342nosgnn0i 32138 . . . . . . . . . 10 ∅ ≠ 1𝑜
4443neii 2987 . . . . . . . . 9 ¬ ∅ = 1𝑜
45 simpll3 1266 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = ∅)
46 simplr 776 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐵𝑋) = 1𝑜)
47 eqeq1 2817 . . . . . . . . . . . . 13 ((𝐴𝑋) = (𝐵𝑋) → ((𝐴𝑋) = ∅ ↔ (𝐵𝑋) = ∅))
4847anbi1d 617 . . . . . . . . . . . 12 ((𝐴𝑋) = (𝐵𝑋) → (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) ↔ ((𝐵𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜)))
49 eqtr2 2833 . . . . . . . . . . . 12 (((𝐵𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) → ∅ = 1𝑜)
5048, 49syl6bi 244 . . . . . . . . . . 11 ((𝐴𝑋) = (𝐵𝑋) → (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) → ∅ = 1𝑜))
5150com12 32 . . . . . . . . . 10 (((𝐴𝑋) = ∅ ∧ (𝐵𝑋) = 1𝑜) → ((𝐴𝑋) = (𝐵𝑋) → ∅ = 1𝑜))
5245, 46, 51syl2anc 575 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋) = (𝐵𝑋) → ∅ = 1𝑜))
5344, 52mtoi 190 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋) = (𝐵𝑋))
54 simpr 473 . . . . . . . . 9 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → 𝑋𝑥)
55 simplrr 787 . . . . . . . . 9 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))
56 fveq2 6411 . . . . . . . . . . 11 (𝑦 = 𝑋 → (𝐴𝑦) = (𝐴𝑋))
57 fveq2 6411 . . . . . . . . . . 11 (𝑦 = 𝑋 → (𝐵𝑦) = (𝐵𝑋))
5856, 57eqeq12d 2828 . . . . . . . . . 10 (𝑦 = 𝑋 → ((𝐴𝑦) = (𝐵𝑦) ↔ (𝐴𝑋) = (𝐵𝑋)))
5958rspcv 3505 . . . . . . . . 9 (𝑋𝑥 → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → (𝐴𝑋) = (𝐵𝑋)))
6054, 55, 59sylc 65 . . . . . . . 8 ((((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) ∧ 𝑋𝑥) → (𝐴𝑋) = (𝐵𝑋))
6153, 60mtand 841 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ 𝑋𝑥)
62 simprl 778 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥 ∈ On)
63 simpl13 1326 . . . . . . . . 9 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) → 𝑋 ∈ On)
6463adantr 468 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑋 ∈ On)
65 ontri1 5977 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
6662, 64, 65syl2anc 575 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 ↔ ¬ 𝑋𝑥))
6761, 66mpbird 248 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → 𝑥𝑋)
68 onsseleq 5984 . . . . . . . 8 ((𝑥 ∈ On ∧ 𝑋 ∈ On) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
6962, 64, 68syl2anc 575 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 ↔ (𝑥𝑋𝑥 = 𝑋)))
70 eqtr2 2833 . . . . . . . . . . . . . 14 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 1𝑜) → ∅ = 1𝑜)
7170ancoms 448 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) → ∅ = 1𝑜)
7244, 71mto 188 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅)
73 df-1o 7799 . . . . . . . . . . . . . . . 16 1𝑜 = suc ∅
74 df-2o 7800 . . . . . . . . . . . . . . . 16 2𝑜 = suc 1𝑜
7573, 74eqeq12i 2827 . . . . . . . . . . . . . . 15 (1𝑜 = 2𝑜 ↔ suc ∅ = suc 1𝑜)
76 0elon 5997 . . . . . . . . . . . . . . . 16 ∅ ∈ On
77 1on 7806 . . . . . . . . . . . . . . . 16 1𝑜 ∈ On
78 suc11 6047 . . . . . . . . . . . . . . . 16 ((∅ ∈ On ∧ 1𝑜 ∈ On) → (suc ∅ = suc 1𝑜 ↔ ∅ = 1𝑜))
7976, 77, 78mp2an 675 . . . . . . . . . . . . . . 15 (suc ∅ = suc 1𝑜 ↔ ∅ = 1𝑜)
8075, 79bitri 266 . . . . . . . . . . . . . 14 (1𝑜 = 2𝑜 ↔ ∅ = 1𝑜)
8143, 80nemtbir 3080 . . . . . . . . . . . . 13 ¬ 1𝑜 = 2𝑜
82 eqtr2 2833 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) → 1𝑜 = 2𝑜)
8381, 82mto 188 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)
84 2on 7808 . . . . . . . . . . . . . . . . 17 2𝑜 ∈ On
8584elexi 3414 . . . . . . . . . . . . . . . 16 2𝑜 ∈ V
8685prid2 4496 . . . . . . . . . . . . . . 15 2𝑜 ∈ {1𝑜, 2𝑜}
8786nosgnn0i 32138 . . . . . . . . . . . . . 14 ∅ ≠ 2𝑜
8887neii 2987 . . . . . . . . . . . . 13 ¬ ∅ = 2𝑜
89 eqtr2 2833 . . . . . . . . . . . . 13 ((((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) → ∅ = 2𝑜)
9088, 89mto 188 . . . . . . . . . . . 12 ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)
9172, 83, 903pm3.2i 1431 . . . . . . . . . . 11 (¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜))
92 fvex 6424 . . . . . . . . . . . . . 14 ((𝐴𝑋)‘𝑥) ∈ V
9392, 92brtp 31966 . . . . . . . . . . . . 13 (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥) ↔ ((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)))
94 3oran 1128 . . . . . . . . . . . . 13 (((((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∨ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∨ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)))
9593, 94bitri 266 . . . . . . . . . . . 12 (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥) ↔ ¬ (¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)))
9695con2bii 348 . . . . . . . . . . 11 ((¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = ∅) ∧ ¬ (((𝐴𝑋)‘𝑥) = 1𝑜 ∧ ((𝐴𝑋)‘𝑥) = 2𝑜) ∧ ¬ (((𝐴𝑋)‘𝑥) = ∅ ∧ ((𝐴𝑋)‘𝑥) = 2𝑜)) ↔ ¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥))
9791, 96mpbi 221 . . . . . . . . . 10 ¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥)
98 simpl2l 1290 . . . . . . . . . . . . 13 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) → (𝐴𝑋) = (𝐵𝑋))
9998adantr 468 . . . . . . . . . . . 12 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝐴𝑋) = (𝐵𝑋))
10099fveq1d 6413 . . . . . . . . . . 11 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋)‘𝑥) = ((𝐵𝑋)‘𝑥))
101100breq2d 4863 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐴𝑋)‘𝑥) ↔ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥)))
10297, 101mtbii 317 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥))
103 fvres 6430 . . . . . . . . . . 11 (𝑥𝑋 → ((𝐴𝑋)‘𝑥) = (𝐴𝑥))
104 fvres 6430 . . . . . . . . . . 11 (𝑥𝑋 → ((𝐵𝑋)‘𝑥) = (𝐵𝑥))
105103, 104breq12d 4864 . . . . . . . . . 10 (𝑥𝑋 → (((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥) ↔ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
106105notbid 309 . . . . . . . . 9 (𝑥𝑋 → (¬ ((𝐴𝑋)‘𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} ((𝐵𝑋)‘𝑥) ↔ ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
107102, 106syl5ibcom 236 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
10844intnanr 477 . . . . . . . . . . . 12 ¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅)
10944intnanr 477 . . . . . . . . . . . 12 ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜)
11081intnan 476 . . . . . . . . . . . 12 ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)
111108, 109, 1103pm3.2i 1431 . . . . . . . . . . 11 (¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜))
112 0ex 4991 . . . . . . . . . . . . . 14 ∅ ∈ V
113112, 41brtp 31966 . . . . . . . . . . . . 13 (∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜 ↔ ((∅ = 1𝑜 ∧ 1𝑜 = ∅) ∨ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∨ (∅ = ∅ ∧ 1𝑜 = 2𝑜)))
114 3oran 1128 . . . . . . . . . . . . 13 (((∅ = 1𝑜 ∧ 1𝑜 = ∅) ∨ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∨ (∅ = ∅ ∧ 1𝑜 = 2𝑜)) ↔ ¬ (¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)))
115113, 114bitri 266 . . . . . . . . . . . 12 (∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜 ↔ ¬ (¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)))
116115con2bii 348 . . . . . . . . . . 11 ((¬ (∅ = 1𝑜 ∧ 1𝑜 = ∅) ∧ ¬ (∅ = 1𝑜 ∧ 1𝑜 = 2𝑜) ∧ ¬ (∅ = ∅ ∧ 1𝑜 = 2𝑜)) ↔ ¬ ∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜)
117111, 116mpbi 221 . . . . . . . . . 10 ¬ ∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜
11845, 46breq12d 4864 . . . . . . . . . 10 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋) ↔ ∅{⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩}1𝑜))
119117, 118mtbiri 318 . . . . . . . . 9 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋))
120 fveq2 6411 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝐴𝑥) = (𝐴𝑋))
121 fveq2 6411 . . . . . . . . . . 11 (𝑥 = 𝑋 → (𝐵𝑥) = (𝐵𝑋))
122120, 121breq12d 4864 . . . . . . . . . 10 (𝑥 = 𝑋 → ((𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ (𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋)))
123122notbid 309 . . . . . . . . 9 (𝑥 = 𝑋 → (¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥) ↔ ¬ (𝐴𝑋){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑋)))
124119, 123syl5ibrcom 238 . . . . . . . 8 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥 = 𝑋 → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
125107, 124jaod 877 . . . . . . 7 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ((𝑥𝑋𝑥 = 𝑋) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
12669, 125sylbid 231 . . . . . 6 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → (𝑥𝑋 → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
12767, 126mpd 15 . . . . 5 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ (𝑥 ∈ On ∧ ∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦))) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥))
128127expr 446 . . . 4 (((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) ∧ 𝑥 ∈ On) → (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
129128ralrimiva 3161 . . 3 ((((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) ∧ (𝐵𝑋) = 1𝑜) → ∀𝑥 ∈ On (∀𝑦𝑥 (𝐴𝑦) = (𝐵𝑦) → ¬ (𝐴𝑥){⟨1𝑜, ∅⟩, ⟨1𝑜, 2𝑜⟩, ⟨∅, 2𝑜⟩} (𝐵𝑥)))
13040, 129mtand 841 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ¬ (𝐵𝑋) = 1𝑜)
131 nofv 32136 . . . 4 (𝐵 No → ((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜))
13232, 131syl 17 . . 3 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜))
133 3orrot 1105 . . . 4 (((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜) ↔ ((𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅))
134 3orrot 1105 . . . 4 (((𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅) ↔ ((𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜))
135133, 134bitri 266 . . 3 (((𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜 ∨ (𝐵𝑋) = 2𝑜) ↔ ((𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜))
136132, 135sylib 209 . 2 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → ((𝐵𝑋) = 2𝑜 ∨ (𝐵𝑋) = ∅ ∨ (𝐵𝑋) = 1𝑜))
13731, 130, 136ecase23d 1590 1 (((𝐴 No 𝐵 No 𝑋 ∈ On) ∧ ((𝐴𝑋) = (𝐵𝑋) ∧ 𝐴 <s 𝐵) ∧ (𝐴𝑋) = ∅) → (𝐵𝑋) = 2𝑜)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3o 1099  w3a 1100   = wceq 1637  wcel 2157  wral 3103  wrex 3104  wss 3776  c0 4123  {ctp 4381  cop 4383   class class class wbr 4851   Or wor 5238  dom cdm 5318  cres 5320  Rel wrel 5323  Oncon0 5943  suc csuc 5945  Fun wfun 6098  cfv 6104  1𝑜c1o 7792  2𝑜c2o 7793   No csur 32119   <s cslt 32120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-ord 5946  df-on 5947  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-1o 7799  df-2o 7800  df-no 32122  df-slt 32123
This theorem is referenced by:  nosupbnd1lem4  32183
  Copyright terms: Public domain W3C validator