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

Theorem isf34lem6 9796
 Description: Lemma for isfin3-4 9798. (Contributed by Stefan O'Rear, 7-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)
Hypothesis
Ref Expression
compss.a 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴𝑥))
Assertion
Ref Expression
isf34lem6 (𝐴𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓)))
Distinct variable groups:   𝑥,𝑓,𝑦,𝐴   𝑓,𝐹,𝑦   𝑥,𝑉,𝑦
Allowed substitution hints:   𝐹(𝑥)   𝑉(𝑓)

Proof of Theorem isf34lem6
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 elmapi 8423 . . . 4 (𝑓 ∈ (𝒫 𝐴m ω) → 𝑓:ω⟶𝒫 𝐴)
2 compss.a . . . . . 6 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴𝑥))
32isf34lem7 9795 . . . . 5 ((𝐴 ∈ FinIII𝑓:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦)) → ran 𝑓 ∈ ran 𝑓)
433expia 1115 . . . 4 ((𝐴 ∈ FinIII𝑓:ω⟶𝒫 𝐴) → (∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓))
51, 4sylan2 592 . . 3 ((𝐴 ∈ FinIII𝑓 ∈ (𝒫 𝐴m ω)) → (∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓))
65ralrimiva 3187 . 2 (𝐴 ∈ FinIII → ∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓))
7 elmapex 8422 . . . . . . . . . . 11 (𝑔 ∈ (𝒫 𝐴m ω) → (𝒫 𝐴 ∈ V ∧ ω ∈ V))
87simpld 495 . . . . . . . . . 10 (𝑔 ∈ (𝒫 𝐴m ω) → 𝒫 𝐴 ∈ V)
9 pwexb 7481 . . . . . . . . . 10 (𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V)
108, 9sylibr 235 . . . . . . . . 9 (𝑔 ∈ (𝒫 𝐴m ω) → 𝐴 ∈ V)
112isf34lem2 9789 . . . . . . . . 9 (𝐴 ∈ V → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
1210, 11syl 17 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐴m ω) → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
13 elmapi 8423 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐴m ω) → 𝑔:ω⟶𝒫 𝐴)
14 fco 6530 . . . . . . . 8 ((𝐹:𝒫 𝐴⟶𝒫 𝐴𝑔:ω⟶𝒫 𝐴) → (𝐹𝑔):ω⟶𝒫 𝐴)
1512, 13, 14syl2anc 584 . . . . . . 7 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹𝑔):ω⟶𝒫 𝐴)
16 elmapg 8414 . . . . . . . 8 ((𝒫 𝐴 ∈ V ∧ ω ∈ V) → ((𝐹𝑔) ∈ (𝒫 𝐴m ω) ↔ (𝐹𝑔):ω⟶𝒫 𝐴))
177, 16syl 17 . . . . . . 7 (𝑔 ∈ (𝒫 𝐴m ω) → ((𝐹𝑔) ∈ (𝒫 𝐴m ω) ↔ (𝐹𝑔):ω⟶𝒫 𝐴))
1815, 17mpbird 258 . . . . . 6 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹𝑔) ∈ (𝒫 𝐴m ω))
19 fveq1 6668 . . . . . . . . . 10 (𝑓 = (𝐹𝑔) → (𝑓𝑦) = ((𝐹𝑔)‘𝑦))
20 fveq1 6668 . . . . . . . . . 10 (𝑓 = (𝐹𝑔) → (𝑓‘suc 𝑦) = ((𝐹𝑔)‘suc 𝑦))
2119, 20sseq12d 4004 . . . . . . . . 9 (𝑓 = (𝐹𝑔) → ((𝑓𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦)))
2221ralbidv 3202 . . . . . . . 8 (𝑓 = (𝐹𝑔) → (∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) ↔ ∀𝑦 ∈ ω ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦)))
23 rneq 5805 . . . . . . . . . . 11 (𝑓 = (𝐹𝑔) → ran 𝑓 = ran (𝐹𝑔))
24 rnco2 6105 . . . . . . . . . . 11 ran (𝐹𝑔) = (𝐹 “ ran 𝑔)
2523, 24syl6eq 2877 . . . . . . . . . 10 (𝑓 = (𝐹𝑔) → ran 𝑓 = (𝐹 “ ran 𝑔))
2625unieqd 4847 . . . . . . . . 9 (𝑓 = (𝐹𝑔) → ran 𝑓 = (𝐹 “ ran 𝑔))
2726, 25eleq12d 2912 . . . . . . . 8 (𝑓 = (𝐹𝑔) → ( ran 𝑓 ∈ ran 𝑓 (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)))
2822, 27imbi12d 346 . . . . . . 7 (𝑓 = (𝐹𝑔) → ((∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓) ↔ (∀𝑦 ∈ ω ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦) → (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔))))
2928rspccv 3624 . . . . . 6 (∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓) → ((𝐹𝑔) ∈ (𝒫 𝐴m ω) → (∀𝑦 ∈ ω ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦) → (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔))))
3018, 29syl5 34 . . . . 5 (∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓) → (𝑔 ∈ (𝒫 𝐴m ω) → (∀𝑦 ∈ ω ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦) → (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔))))
31 sscon 4119 . . . . . . . . 9 ((𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → (𝐴 ∖ (𝑔𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦)))
3213ffvelrnda 6849 . . . . . . . . . . . 12 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → (𝑔𝑦) ∈ 𝒫 𝐴)
3332elpwid 4556 . . . . . . . . . . 11 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → (𝑔𝑦) ⊆ 𝐴)
342isf34lem1 9788 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ (𝑔𝑦) ⊆ 𝐴) → (𝐹‘(𝑔𝑦)) = (𝐴 ∖ (𝑔𝑦)))
3510, 33, 34syl2an2r 681 . . . . . . . . . 10 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → (𝐹‘(𝑔𝑦)) = (𝐴 ∖ (𝑔𝑦)))
36 peano2 7595 . . . . . . . . . . . . 13 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
37 ffvelrn 6847 . . . . . . . . . . . . 13 ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → (𝑔‘suc 𝑦) ∈ 𝒫 𝐴)
3813, 36, 37syl2an 595 . . . . . . . . . . . 12 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → (𝑔‘suc 𝑦) ∈ 𝒫 𝐴)
3938elpwid 4556 . . . . . . . . . . 11 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → (𝑔‘suc 𝑦) ⊆ 𝐴)
402isf34lem1 9788 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ (𝑔‘suc 𝑦) ⊆ 𝐴) → (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦)))
4110, 39, 40syl2an2r 681 . . . . . . . . . 10 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → (𝐹‘(𝑔‘suc 𝑦)) = (𝐴 ∖ (𝑔‘suc 𝑦)))
4235, 41sseq12d 4004 . . . . . . . . 9 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → ((𝐹‘(𝑔𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦)) ↔ (𝐴 ∖ (𝑔𝑦)) ⊆ (𝐴 ∖ (𝑔‘suc 𝑦))))
4331, 42syl5ibr 247 . . . . . . . 8 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → ((𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → (𝐹‘(𝑔𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦))))
44 fvco3 6759 . . . . . . . . . 10 ((𝑔:ω⟶𝒫 𝐴𝑦 ∈ ω) → ((𝐹𝑔)‘𝑦) = (𝐹‘(𝑔𝑦)))
4513, 44sylan 580 . . . . . . . . 9 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → ((𝐹𝑔)‘𝑦) = (𝐹‘(𝑔𝑦)))
46 fvco3 6759 . . . . . . . . . 10 ((𝑔:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → ((𝐹𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦)))
4713, 36, 46syl2an 595 . . . . . . . . 9 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → ((𝐹𝑔)‘suc 𝑦) = (𝐹‘(𝑔‘suc 𝑦)))
4845, 47sseq12d 4004 . . . . . . . 8 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → (((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦) ↔ (𝐹‘(𝑔𝑦)) ⊆ (𝐹‘(𝑔‘suc 𝑦))))
4943, 48sylibrd 260 . . . . . . 7 ((𝑔 ∈ (𝒫 𝐴m ω) ∧ 𝑦 ∈ ω) → ((𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦)))
5049ralimdva 3182 . . . . . 6 (𝑔 ∈ (𝒫 𝐴m ω) → (∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → ∀𝑦 ∈ ω ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦)))
5112ffnd 6514 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐴m ω) → 𝐹 Fn 𝒫 𝐴)
52 imassrn 5939 . . . . . . . . 9 (𝐹 “ ran 𝑔) ⊆ ran 𝐹
5312frnd 6520 . . . . . . . . 9 (𝑔 ∈ (𝒫 𝐴m ω) → ran 𝐹 ⊆ 𝒫 𝐴)
5452, 53sstrid 3982 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴)
55 fnfvima 6991 . . . . . . . . 9 ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)) → (𝐹 (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)))
56553expia 1115 . . . . . . . 8 ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴) → ( (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹 (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔))))
5751, 54, 56syl2anc 584 . . . . . . 7 (𝑔 ∈ (𝒫 𝐴m ω) → ( (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → (𝐹 (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔))))
58 incom 4182 . . . . . . . . . . . . 13 (dom 𝐹 ∩ ran 𝑔) = (ran 𝑔 ∩ dom 𝐹)
5913frnd 6520 . . . . . . . . . . . . . . 15 (𝑔 ∈ (𝒫 𝐴m ω) → ran 𝑔 ⊆ 𝒫 𝐴)
6012fdmd 6522 . . . . . . . . . . . . . . 15 (𝑔 ∈ (𝒫 𝐴m ω) → dom 𝐹 = 𝒫 𝐴)
6159, 60sseqtrrd 4012 . . . . . . . . . . . . . 14 (𝑔 ∈ (𝒫 𝐴m ω) → ran 𝑔 ⊆ dom 𝐹)
62 df-ss 3956 . . . . . . . . . . . . . 14 (ran 𝑔 ⊆ dom 𝐹 ↔ (ran 𝑔 ∩ dom 𝐹) = ran 𝑔)
6361, 62sylib 219 . . . . . . . . . . . . 13 (𝑔 ∈ (𝒫 𝐴m ω) → (ran 𝑔 ∩ dom 𝐹) = ran 𝑔)
6458, 63syl5eq 2873 . . . . . . . . . . . 12 (𝑔 ∈ (𝒫 𝐴m ω) → (dom 𝐹 ∩ ran 𝑔) = ran 𝑔)
6513fdmd 6522 . . . . . . . . . . . . . 14 (𝑔 ∈ (𝒫 𝐴m ω) → dom 𝑔 = ω)
66 peano1 7594 . . . . . . . . . . . . . . 15 ∅ ∈ ω
67 ne0i 4304 . . . . . . . . . . . . . . 15 (∅ ∈ ω → ω ≠ ∅)
6866, 67mp1i 13 . . . . . . . . . . . . . 14 (𝑔 ∈ (𝒫 𝐴m ω) → ω ≠ ∅)
6965, 68eqnetrd 3088 . . . . . . . . . . . . 13 (𝑔 ∈ (𝒫 𝐴m ω) → dom 𝑔 ≠ ∅)
70 dm0rn0 5794 . . . . . . . . . . . . . 14 (dom 𝑔 = ∅ ↔ ran 𝑔 = ∅)
7170necon3bii 3073 . . . . . . . . . . . . 13 (dom 𝑔 ≠ ∅ ↔ ran 𝑔 ≠ ∅)
7269, 71sylib 219 . . . . . . . . . . . 12 (𝑔 ∈ (𝒫 𝐴m ω) → ran 𝑔 ≠ ∅)
7364, 72eqnetrd 3088 . . . . . . . . . . 11 (𝑔 ∈ (𝒫 𝐴m ω) → (dom 𝐹 ∩ ran 𝑔) ≠ ∅)
74 imadisj 5947 . . . . . . . . . . . 12 ((𝐹 “ ran 𝑔) = ∅ ↔ (dom 𝐹 ∩ ran 𝑔) = ∅)
7574necon3bii 3073 . . . . . . . . . . 11 ((𝐹 “ ran 𝑔) ≠ ∅ ↔ (dom 𝐹 ∩ ran 𝑔) ≠ ∅)
7673, 75sylibr 235 . . . . . . . . . 10 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹 “ ran 𝑔) ≠ ∅)
772isf34lem4 9793 . . . . . . . . . 10 ((𝐴 ∈ V ∧ ((𝐹 “ ran 𝑔) ⊆ 𝒫 𝐴 ∧ (𝐹 “ ran 𝑔) ≠ ∅)) → (𝐹 (𝐹 “ ran 𝑔)) = (𝐹 “ (𝐹 “ ran 𝑔)))
7810, 54, 76, 77syl12anc 834 . . . . . . . . 9 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹 (𝐹 “ ran 𝑔)) = (𝐹 “ (𝐹 “ ran 𝑔)))
792isf34lem3 9791 . . . . . . . . . . 11 ((𝐴 ∈ V ∧ ran 𝑔 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔)
8010, 59, 79syl2anc 584 . . . . . . . . . 10 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔)
8180inteqd 4879 . . . . . . . . 9 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹 “ (𝐹 “ ran 𝑔)) = ran 𝑔)
8278, 81eqtrd 2861 . . . . . . . 8 (𝑔 ∈ (𝒫 𝐴m ω) → (𝐹 (𝐹 “ ran 𝑔)) = ran 𝑔)
8382, 80eleq12d 2912 . . . . . . 7 (𝑔 ∈ (𝒫 𝐴m ω) → ((𝐹 (𝐹 “ ran 𝑔)) ∈ (𝐹 “ (𝐹 “ ran 𝑔)) ↔ ran 𝑔 ∈ ran 𝑔))
8457, 83sylibd 240 . . . . . 6 (𝑔 ∈ (𝒫 𝐴m ω) → ( (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔) → ran 𝑔 ∈ ran 𝑔))
8550, 84imim12d 81 . . . . 5 (𝑔 ∈ (𝒫 𝐴m ω) → ((∀𝑦 ∈ ω ((𝐹𝑔)‘𝑦) ⊆ ((𝐹𝑔)‘suc 𝑦) → (𝐹 “ ran 𝑔) ∈ (𝐹 “ ran 𝑔)) → (∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → ran 𝑔 ∈ ran 𝑔)))
8630, 85sylcom 30 . . . 4 (∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓) → (𝑔 ∈ (𝒫 𝐴m ω) → (∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → ran 𝑔 ∈ ran 𝑔)))
8786ralrimiv 3186 . . 3 (∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓) → ∀𝑔 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → ran 𝑔 ∈ ran 𝑔))
88 isfin3-3 9784 . . 3 (𝐴𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑔 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑔‘suc 𝑦) ⊆ (𝑔𝑦) → ran 𝑔 ∈ ran 𝑔)))
8987, 88syl5ibr 247 . 2 (𝐴𝑉 → (∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓) → 𝐴 ∈ FinIII))
906, 89impbid2 227 1 (𝐴𝑉 → (𝐴 ∈ FinIII ↔ ∀𝑓 ∈ (𝒫 𝐴m ω)(∀𝑦 ∈ ω (𝑓𝑦) ⊆ (𝑓‘suc 𝑦) → ran 𝑓 ∈ ran 𝑓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1530   ∈ wcel 2107   ≠ wne 3021  ∀wral 3143  Vcvv 3500   ∖ cdif 3937   ∩ cin 3939   ⊆ wss 3940  ∅c0 4295  𝒫 cpw 4542  ∪ cuni 4837  ∩ cint 4874   ↦ cmpt 5143  dom cdm 5554  ran crn 5555   “ cima 5557   ∘ ccom 5558  suc csuc 6192   Fn wfn 6349  ⟶wf 6350  ‘cfv 6354  (class class class)co 7150  ωcom 7573   ↑m cmap 8401  FinIIIcfin3 9697 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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-lim 6195  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-rpss 7443  df-om 7574  df-1st 7685  df-2nd 7686  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-seqom 8080  df-1o 8098  df-oadd 8102  df-er 8284  df-map 8403  df-en 8504  df-dom 8505  df-sdom 8506  df-fin 8507  df-wdom 9017  df-card 9362  df-fin4 9703  df-fin3 9704 This theorem is referenced by:  isfin3-4  9798
 Copyright terms: Public domain W3C validator