isf34lem7 - Metamath Proof Explorer

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

Theorem isf34lem7 9201

Description: Lemma for isfin3-4 9204. (Contributed by Stefan O'Rear, 7-Nov-2014.)

**Hypothesis**
Ref	Expression
compss.a	⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))

**Assertion**
Ref	Expression
isf34lem7	⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∪ ran 𝐺 ∈ ran 𝐺)

Distinct variable groups: 𝑥,𝑦,𝐴 𝑦,𝐹 𝑦,𝐺 Allowed substitution hints: 𝐹(𝑥) 𝐺(𝑥)

**Proof of Theorem isf34lem7**
Step	Hyp	Ref	Expression
1		compss.a	. . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴 ∖ 𝑥))
2	1	isf34lem2 9195	. . . . . 6 ⊢ (𝐴 ∈ Fin^III → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
3	2	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
4	3	3adant3 1081	. . . 4 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
5		ffn 6045	. . . 4 ⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → 𝐹 Fn 𝒫 𝐴)
6	4, 5	syl 17	. . 3 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → 𝐹 Fn 𝒫 𝐴)
7		imassrn 5477	. . . 4 ⊢ (𝐹 “ ran 𝐺) ⊆ ran 𝐹
8		frn 6053	. . . . . 6 ⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → ran 𝐹 ⊆ 𝒫 𝐴)
9	3, 8	syl 17	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → ran 𝐹 ⊆ 𝒫 𝐴)
10	9	3adant3 1081	. . . 4 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ran 𝐹 ⊆ 𝒫 𝐴)
11	7, 10	syl5ss 3614	. . 3 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → (𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴)
12		simp1 1061	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → 𝐴 ∈ Fin^III)
13		fco 6058	. . . . . . 7 ⊢ ((𝐹:𝒫 𝐴⟶𝒫 𝐴 ∧ 𝐺:ω⟶𝒫 𝐴) → (𝐹 ∘ 𝐺):ω⟶𝒫 𝐴)
14	2, 13	sylan 488	. . . . . 6 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (𝐹 ∘ 𝐺):ω⟶𝒫 𝐴)
15	14	3adant3 1081	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → (𝐹 ∘ 𝐺):ω⟶𝒫 𝐴)
16		sscon 3744	. . . . . . . 8 ⊢ ((𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴 ∖ (𝐺‘suc 𝑦)) ⊆ (𝐴 ∖ (𝐺‘𝑦)))
17		simpr 477	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → 𝐺:ω⟶𝒫 𝐴)
18		peano2 7086	. . . . . . . . . . 11 ⊢ (𝑦 ∈ ω → suc 𝑦 ∈ ω)
19		fvco3 6275	. . . . . . . . . . 11 ⊢ ((𝐺:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → ((𝐹 ∘ 𝐺)‘suc 𝑦) = (𝐹‘(𝐺‘suc 𝑦)))
20	17, 18, 19	syl2an 494	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝐺)‘suc 𝑦) = (𝐹‘(𝐺‘suc 𝑦)))
21		simpll 790	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → 𝐴 ∈ Fin^III)
22		ffvelrn 6357	. . . . . . . . . . . . 13 ⊢ ((𝐺:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → (𝐺‘suc 𝑦) ∈ 𝒫 𝐴)
23	17, 18, 22	syl2an 494	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺‘suc 𝑦) ∈ 𝒫 𝐴)
24	23	elpwid 4170	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺‘suc 𝑦) ⊆ 𝐴)
25	1	isf34lem1 9194	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin^III ∧ (𝐺‘suc 𝑦) ⊆ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) = (𝐴 ∖ (𝐺‘suc 𝑦)))
26	21, 24, 25	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐹‘(𝐺‘suc 𝑦)) = (𝐴 ∖ (𝐺‘suc 𝑦)))
27	20, 26	eqtrd 2656	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝐺)‘suc 𝑦) = (𝐴 ∖ (𝐺‘suc 𝑦)))
28		fvco3 6275	. . . . . . . . . . 11 ⊢ ((𝐺:ω⟶𝒫 𝐴 ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦)))
29	28	adantll 750	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦)))
30		ffvelrn 6357	. . . . . . . . . . . . 13 ⊢ ((𝐺:ω⟶𝒫 𝐴 ∧ 𝑦 ∈ ω) → (𝐺‘𝑦) ∈ 𝒫 𝐴)
31	30	adantll 750	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺‘𝑦) ∈ 𝒫 𝐴)
32	31	elpwid 4170	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺‘𝑦) ⊆ 𝐴)
33	1	isf34lem1 9194	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin^III ∧ (𝐺‘𝑦) ⊆ 𝐴) → (𝐹‘(𝐺‘𝑦)) = (𝐴 ∖ (𝐺‘𝑦)))
34	21, 32, 33	syl2anc 693	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐹‘(𝐺‘𝑦)) = (𝐴 ∖ (𝐺‘𝑦)))
35	29, 34	eqtrd 2656	. . . . . . . . 9 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐴 ∖ (𝐺‘𝑦)))
36	27, 35	sseq12d 3634	. . . . . . . 8 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (((𝐹 ∘ 𝐺)‘suc 𝑦) ⊆ ((𝐹 ∘ 𝐺)‘𝑦) ↔ (𝐴 ∖ (𝐺‘suc 𝑦)) ⊆ (𝐴 ∖ (𝐺‘𝑦))))
37	16, 36	syl5ibr 236	. . . . . . 7 ⊢ (((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → ((𝐹 ∘ 𝐺)‘suc 𝑦) ⊆ ((𝐹 ∘ 𝐺)‘𝑦)))
38	37	ralimdva 2962	. . . . . 6 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → ∀𝑦 ∈ ω ((𝐹 ∘ 𝐺)‘suc 𝑦) ⊆ ((𝐹 ∘ 𝐺)‘𝑦)))
39	38	3impia 1261	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∀𝑦 ∈ ω ((𝐹 ∘ 𝐺)‘suc 𝑦) ⊆ ((𝐹 ∘ 𝐺)‘𝑦))
40		fin33i 9191	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ (𝐹 ∘ 𝐺):ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω ((𝐹 ∘ 𝐺)‘suc 𝑦) ⊆ ((𝐹 ∘ 𝐺)‘𝑦)) → ∩ ran (𝐹 ∘ 𝐺) ∈ ran (𝐹 ∘ 𝐺))
41	12, 15, 39, 40	syl3anc 1326	. . . 4 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∩ ran (𝐹 ∘ 𝐺) ∈ ran (𝐹 ∘ 𝐺))
42		rnco2 5642	. . . . 5 ⊢ ran (𝐹 ∘ 𝐺) = (𝐹 “ ran 𝐺)
43	42	inteqi 4479	. . . 4 ⊢ ∩ ran (𝐹 ∘ 𝐺) = ∩ (𝐹 “ ran 𝐺)
44	41, 43, 42	3eltr3g 2717	. . 3 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∩ (𝐹 “ ran 𝐺) ∈ (𝐹 “ ran 𝐺))
45		fnfvima 6496	. . 3 ⊢ ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴 ∧ ∩ (𝐹 “ ran 𝐺) ∈ (𝐹 “ ran 𝐺)) → (𝐹‘∩ (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)))
46	6, 11, 44, 45	syl3anc 1326	. 2 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → (𝐹‘∩ (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)))
47		simpl 473	. . . . . 6 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → 𝐴 ∈ Fin^III)
48	7, 9	syl5ss 3614	. . . . . 6 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴)
49		incom 3805	. . . . . . . . 9 ⊢ (dom 𝐹 ∩ ran 𝐺) = (ran 𝐺 ∩ dom 𝐹)
50		frn 6053	. . . . . . . . . . . 12 ⊢ (𝐺:ω⟶𝒫 𝐴 → ran 𝐺 ⊆ 𝒫 𝐴)
51	50	adantl 482	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → ran 𝐺 ⊆ 𝒫 𝐴)
52		fdm 6051	. . . . . . . . . . . 12 ⊢ (𝐹:𝒫 𝐴⟶𝒫 𝐴 → dom 𝐹 = 𝒫 𝐴)
53	3, 52	syl 17	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → dom 𝐹 = 𝒫 𝐴)
54	51, 53	sseqtr4d 3642	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → ran 𝐺 ⊆ dom 𝐹)
55		df-ss 3588	. . . . . . . . . 10 ⊢ (ran 𝐺 ⊆ dom 𝐹 ↔ (ran 𝐺 ∩ dom 𝐹) = ran 𝐺)
56	54, 55	sylib 208	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (ran 𝐺 ∩ dom 𝐹) = ran 𝐺)
57	49, 56	syl5eq 2668	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (dom 𝐹 ∩ ran 𝐺) = ran 𝐺)
58		fdm 6051	. . . . . . . . . . 11 ⊢ (𝐺:ω⟶𝒫 𝐴 → dom 𝐺 = ω)
59	58	adantl 482	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → dom 𝐺 = ω)
60		peano1 7085	. . . . . . . . . . 11 ⊢ ∅ ∈ ω
61		ne0i 3921	. . . . . . . . . . 11 ⊢ (∅ ∈ ω → ω ≠ ∅)
62	60, 61	mp1i 13	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → ω ≠ ∅)
63	59, 62	eqnetrd 2861	. . . . . . . . 9 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → dom 𝐺 ≠ ∅)
64		dm0rn0 5342	. . . . . . . . . 10 ⊢ (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
65	64	necon3bii 2846	. . . . . . . . 9 ⊢ (dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅)
66	63, 65	sylib 208	. . . . . . . 8 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → ran 𝐺 ≠ ∅)
67	57, 66	eqnetrd 2861	. . . . . . 7 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (dom 𝐹 ∩ ran 𝐺) ≠ ∅)
68		imadisj 5484	. . . . . . . 8 ⊢ ((𝐹 “ ran 𝐺) = ∅ ↔ (dom 𝐹 ∩ ran 𝐺) = ∅)
69	68	necon3bii 2846	. . . . . . 7 ⊢ ((𝐹 “ ran 𝐺) ≠ ∅ ↔ (dom 𝐹 ∩ ran 𝐺) ≠ ∅)
70	67, 69	sylibr 224	. . . . . 6 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (𝐹 “ ran 𝐺) ≠ ∅)
71	1	isf34lem5 9200	. . . . . 6 ⊢ ((𝐴 ∈ Fin^III ∧ ((𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴 ∧ (𝐹 “ ran 𝐺) ≠ ∅)) → (𝐹‘∩ (𝐹 “ ran 𝐺)) = ∪ (𝐹 “ (𝐹 “ ran 𝐺)))
72	47, 48, 70, 71	syl12anc 1324	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (𝐹‘∩ (𝐹 “ ran 𝐺)) = ∪ (𝐹 “ (𝐹 “ ran 𝐺)))
73	1	isf34lem3 9197	. . . . . . 7 ⊢ ((𝐴 ∈ Fin^III ∧ ran 𝐺 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝐺)) = ran 𝐺)
74	47, 51, 73	syl2anc 693	. . . . . 6 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝐺)) = ran 𝐺)
75	74	unieqd 4446	. . . . 5 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → ∪ (𝐹 “ (𝐹 “ ran 𝐺)) = ∪ ran 𝐺)
76	72, 75	eqtrd 2656	. . . 4 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → (𝐹‘∩ (𝐹 “ ran 𝐺)) = ∪ ran 𝐺)
77	76, 74	eleq12d 2695	. . 3 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴) → ((𝐹‘∩ (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)) ↔ ∪ ran 𝐺 ∈ ran 𝐺))
78	77	3adant3 1081	. 2 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ((𝐹‘∩ (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)) ↔ ∪ ran 𝐺 ∈ ran 𝐺))
79	46, 78	mpbid 222	1 ⊢ ((𝐴 ∈ Fin^III ∧ 𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) → ∪ ran 𝐺 ∈ ran 𝐺)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∖ cdif 3571 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 ∪ cuni 4436 ∩ cint 4475 ↦ cmpt 4729 dom cdm 5114 ran crn 5115 “ cima 5117 ∘ ccom 5118 suc csuc 5725 Fn wfn 5883 ⟶wf 5884 ‘cfv 5888 ωcom 7065 Fin^IIIcfin3 9103

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-rpss 6937 df-om 7066 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-wdom 8464 df-card 8765 df-fin4 9109 df-fin3 9110

This theorem is referenced by: isf34lem6 9202 fin34i 9203

W3C validator