ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  unsnfidcel GIF version

Theorem unsnfidcel 6466
Description: The ¬ 𝐵𝐴 condition in unsnfi 6464. This is intended to show that unsnfi 6464 without that condition would not be provable but it probably would need to be strengthened (for example, to imply included middle) to fully show that. (Contributed by Jim Kingdon, 6-Feb-2022.)
Assertion
Ref Expression
unsnfidcel ((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵𝐴)

Proof of Theorem unsnfidcel
Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isfi 6330 . . . . 5 (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴𝑛)
21biimpi 118 . . . 4 (𝐴 ∈ Fin → ∃𝑛 ∈ ω 𝐴𝑛)
323ad2ant1 960 . . 3 ((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → ∃𝑛 ∈ ω 𝐴𝑛)
4 isfi 6330 . . . . . . 7 ((𝐴 ∪ {𝐵}) ∈ Fin ↔ ∃𝑚 ∈ ω (𝐴 ∪ {𝐵}) ≈ 𝑚)
54biimpi 118 . . . . . 6 ((𝐴 ∪ {𝐵}) ∈ Fin → ∃𝑚 ∈ ω (𝐴 ∪ {𝐵}) ≈ 𝑚)
653ad2ant3 962 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → ∃𝑚 ∈ ω (𝐴 ∪ {𝐵}) ≈ 𝑚)
76adantr 270 . . . 4 (((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) → ∃𝑚 ∈ ω (𝐴 ∪ {𝐵}) ≈ 𝑚)
8 simprr 499 . . . . . . . . . 10 ((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) → (𝐴 ∪ {𝐵}) ≈ 𝑚)
98ad2antrr 472 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → (𝐴 ∪ {𝐵}) ≈ 𝑚)
10 simprr 499 . . . . . . . . . . . 12 (((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) → 𝐴𝑛)
1110ad3antrrr 476 . . . . . . . . . . 11 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝐴𝑛)
12 simplr 497 . . . . . . . . . . 11 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝑚 = 𝑛)
1311, 12breqtrrd 3832 . . . . . . . . . 10 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝐴𝑚)
1413ensymd 6352 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝑚𝐴)
15 entr 6353 . . . . . . . . 9 (((𝐴 ∪ {𝐵}) ≈ 𝑚𝑚𝐴) → (𝐴 ∪ {𝐵}) ≈ 𝐴)
169, 14, 15syl2anc 403 . . . . . . . 8 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → (𝐴 ∪ {𝐵}) ≈ 𝐴)
1716ensymd 6352 . . . . . . 7 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝐴 ≈ (𝐴 ∪ {𝐵}))
18 simp1 939 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → 𝐴 ∈ Fin)
1918ad4antr 478 . . . . . . . 8 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝐴 ∈ Fin)
20 simpl2 943 . . . . . . . . . . 11 (((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) → 𝐵𝑉)
2120ad3antrrr 476 . . . . . . . . . 10 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝐵𝑉)
2221elexd 2621 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝐵 ∈ V)
23 simpr 108 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → ¬ 𝐵𝐴)
2422, 23eldifd 2993 . . . . . . . 8 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → 𝐵 ∈ (V ∖ 𝐴))
25 php5fin 6439 . . . . . . . 8 ((𝐴 ∈ Fin ∧ 𝐵 ∈ (V ∖ 𝐴)) → ¬ 𝐴 ≈ (𝐴 ∪ {𝐵}))
2619, 24, 25syl2anc 403 . . . . . . 7 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) ∧ ¬ 𝐵𝐴) → ¬ 𝐴 ≈ (𝐴 ∪ {𝐵}))
2717, 26pm2.65da 620 . . . . . 6 (((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) → ¬ ¬ 𝐵𝐴)
2827olcd 686 . . . . 5 (((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ 𝑚 = 𝑛) → (¬ 𝐵𝐴 ∨ ¬ ¬ 𝐵𝐴))
298ad2antrr 472 . . . . . . . . . . 11 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → (𝐴 ∪ {𝐵}) ≈ 𝑚)
30 snssi 3550 . . . . . . . . . . . . . 14 (𝐵𝐴 → {𝐵} ⊆ 𝐴)
31 ssequn2 3156 . . . . . . . . . . . . . 14 ({𝐵} ⊆ 𝐴 ↔ (𝐴 ∪ {𝐵}) = 𝐴)
3230, 31sylib 120 . . . . . . . . . . . . 13 (𝐵𝐴 → (𝐴 ∪ {𝐵}) = 𝐴)
3332breq1d 3816 . . . . . . . . . . . 12 (𝐵𝐴 → ((𝐴 ∪ {𝐵}) ≈ 𝑚𝐴𝑚))
3433adantl 271 . . . . . . . . . . 11 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → ((𝐴 ∪ {𝐵}) ≈ 𝑚𝐴𝑚))
3529, 34mpbid 145 . . . . . . . . . 10 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → 𝐴𝑚)
3635ensymd 6352 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → 𝑚𝐴)
3710ad3antrrr 476 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → 𝐴𝑛)
38 entr 6353 . . . . . . . . 9 ((𝑚𝐴𝐴𝑛) → 𝑚𝑛)
3936, 37, 38syl2anc 403 . . . . . . . 8 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → 𝑚𝑛)
40 simprl 498 . . . . . . . . . 10 ((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) → 𝑚 ∈ ω)
4140ad2antrr 472 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → 𝑚 ∈ ω)
42 simprl 498 . . . . . . . . . 10 (((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) → 𝑛 ∈ ω)
4342ad3antrrr 476 . . . . . . . . 9 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → 𝑛 ∈ ω)
44 nneneq 6414 . . . . . . . . 9 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛𝑚 = 𝑛))
4541, 43, 44syl2anc 403 . . . . . . . 8 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → (𝑚𝑛𝑚 = 𝑛))
4639, 45mpbid 145 . . . . . . 7 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → 𝑚 = 𝑛)
47 simplr 497 . . . . . . 7 ((((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) ∧ 𝐵𝐴) → ¬ 𝑚 = 𝑛)
4846, 47pm2.65da 620 . . . . . 6 (((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) → ¬ 𝐵𝐴)
4948orcd 685 . . . . 5 (((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) ∧ ¬ 𝑚 = 𝑛) → (¬ 𝐵𝐴 ∨ ¬ ¬ 𝐵𝐴))
5042adantr 270 . . . . . . 7 ((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) → 𝑛 ∈ ω)
51 nndceq 6164 . . . . . . 7 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → DECID 𝑚 = 𝑛)
5240, 50, 51syl2anc 403 . . . . . 6 ((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) → DECID 𝑚 = 𝑛)
53 exmiddc 778 . . . . . 6 (DECID 𝑚 = 𝑛 → (𝑚 = 𝑛 ∨ ¬ 𝑚 = 𝑛))
5452, 53syl 14 . . . . 5 ((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) → (𝑚 = 𝑛 ∨ ¬ 𝑚 = 𝑛))
5528, 49, 54mpjaodan 745 . . . 4 ((((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) ∧ (𝑚 ∈ ω ∧ (𝐴 ∪ {𝐵}) ≈ 𝑚)) → (¬ 𝐵𝐴 ∨ ¬ ¬ 𝐵𝐴))
567, 55rexlimddv 2486 . . 3 (((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) ∧ (𝑛 ∈ ω ∧ 𝐴𝑛)) → (¬ 𝐵𝐴 ∨ ¬ ¬ 𝐵𝐴))
573, 56rexlimddv 2486 . 2 ((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → (¬ 𝐵𝐴 ∨ ¬ ¬ 𝐵𝐴))
58 df-dc 777 . 2 (DECID ¬ 𝐵𝐴 ↔ (¬ 𝐵𝐴 ∨ ¬ ¬ 𝐵𝐴))
5957, 58sylibr 132 1 ((𝐴 ∈ Fin ∧ 𝐵𝑉 ∧ (𝐴 ∪ {𝐵}) ∈ Fin) → DECID ¬ 𝐵𝐴)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662  DECID wdc 776  w3a 920   = wceq 1285  wcel 1434  wrex 2354  Vcvv 2610  cdif 2980  cun 2981  wss 2983  {csn 3417   class class class wbr 3806  ωcom 4360  cen 6307  Fincfn 6309
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3917  ax-nul 3925  ax-pow 3969  ax-pr 3993  ax-un 4217  ax-setind 4309  ax-iinf 4358
This theorem depends on definitions:  df-bi 115  df-dc 777  df-3or 921  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2612  df-sbc 2826  df-dif 2985  df-un 2987  df-in 2989  df-ss 2996  df-nul 3269  df-pw 3403  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-int 3658  df-br 3807  df-opab 3861  df-tr 3897  df-id 4077  df-iord 4150  df-on 4152  df-suc 4155  df-iom 4361  df-xp 4398  df-rel 4399  df-cnv 4400  df-co 4401  df-dm 4402  df-rn 4403  df-res 4404  df-ima 4405  df-iota 4918  df-fun 4955  df-fn 4956  df-f 4957  df-f1 4958  df-fo 4959  df-f1o 4960  df-fv 4961  df-1o 6086  df-er 6194  df-en 6310  df-fin 6312
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator