isf34lem7

		Ref	Expression
	Hypothesis	compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
	Assertion	isf34lem7	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ∪ ran 𝐺 ∈ ran 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2	1	isf34lem2	⊢ ( 𝐴 ∈ Fin^III → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
3	2	adantr	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
4	3	3adant3	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 )
5	4	ffnd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → 𝐹 Fn 𝒫 𝐴 )
6		imassrn	⊢ ( 𝐹 “ ran 𝐺 ) ⊆ ran 𝐹
7	3	frnd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ran 𝐹 ⊆ 𝒫 𝐴 )
8	7	3adant3	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ran 𝐹 ⊆ 𝒫 𝐴 )
9	6 8	sstrid	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ( 𝐹 “ ran 𝐺 ) ⊆ 𝒫 𝐴 )
10		simp1	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → 𝐴 ∈ Fin^III )
11		fco	⊢ ( ( 𝐹 : 𝒫 𝐴 ⟶ 𝒫 𝐴 ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 ∘ 𝐺 ) : ω ⟶ 𝒫 𝐴 )
12	2 11	sylan	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 ∘ 𝐺 ) : ω ⟶ 𝒫 𝐴 )
13	12	3adant3	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ( 𝐹 ∘ 𝐺 ) : ω ⟶ 𝒫 𝐴 )
14		sscon	⊢ ( ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) → ( 𝐴 ∖ ( 𝐺 ‘ suc 𝑦 ) ) ⊆ ( 𝐴 ∖ ( 𝐺 ‘ 𝑦 ) ) )
15		simpr	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → 𝐺 : ω ⟶ 𝒫 𝐴 )
16		peano2	⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
17		fvco3	⊢ ( ( 𝐺 : ω ⟶ 𝒫 𝐴 ∧ suc 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) )
18	15 16 17	syl2an	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) )
19		simpll	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → 𝐴 ∈ Fin^III )
20		ffvelrn	⊢ ( ( 𝐺 : ω ⟶ 𝒫 𝐴 ∧ suc 𝑦 ∈ ω ) → ( 𝐺 ‘ suc 𝑦 ) ∈ 𝒫 𝐴 )
21	15 16 20	syl2an	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ suc 𝑦 ) ∈ 𝒫 𝐴 )
22	21	elpwid	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ suc 𝑦 ) ⊆ 𝐴 )
23	1	isf34lem1	⊢ ( ( 𝐴 ∈ Fin^III ∧ ( 𝐺 ‘ suc 𝑦 ) ⊆ 𝐴 ) → ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) = ( 𝐴 ∖ ( 𝐺 ‘ suc 𝑦 ) ) )
24	19 22 23	syl2anc	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( 𝐹 ‘ ( 𝐺 ‘ suc 𝑦 ) ) = ( 𝐴 ∖ ( 𝐺 ‘ suc 𝑦 ) ) )
25	18 24	eqtrd	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) = ( 𝐴 ∖ ( 𝐺 ‘ suc 𝑦 ) ) )
26		fvco3	⊢ ( ( 𝐺 : ω ⟶ 𝒫 𝐴 ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
27	26	adantll	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) )
28		ffvelrn	⊢ ( ( 𝐺 : ω ⟶ 𝒫 𝐴 ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝒫 𝐴 )
29	28	adantll	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝒫 𝐴 )
30	29	elpwid	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ 𝑦 ) ⊆ 𝐴 )
31	1	isf34lem1	⊢ ( ( 𝐴 ∈ Fin^III ∧ ( 𝐺 ‘ 𝑦 ) ⊆ 𝐴 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) = ( 𝐴 ∖ ( 𝐺 ‘ 𝑦 ) ) )
32	19 30 31	syl2anc	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) = ( 𝐴 ∖ ( 𝐺 ‘ 𝑦 ) ) )
33	27 32	eqtrd	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) = ( 𝐴 ∖ ( 𝐺 ‘ 𝑦 ) ) )
34	25 33	sseq12d	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ↔ ( 𝐴 ∖ ( 𝐺 ‘ suc 𝑦 ) ) ⊆ ( 𝐴 ∖ ( 𝐺 ‘ 𝑦 ) ) ) )
35	14 34	syl5ibr	⊢ ( ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) ∧ 𝑦 ∈ ω ) → ( ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) → ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
36	35	ralimdva	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) → ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) )
37	36	3impia	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) )
38		fin33i	⊢ ( ( 𝐴 ∈ Fin^III ∧ ( 𝐹 ∘ 𝐺 ) : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( ( 𝐹 ∘ 𝐺 ) ‘ suc 𝑦 ) ⊆ ( ( 𝐹 ∘ 𝐺 ) ‘ 𝑦 ) ) → ∩ ran ( 𝐹 ∘ 𝐺 ) ∈ ran ( 𝐹 ∘ 𝐺 ) )
39	10 13 37 38	syl3anc	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ∩ ran ( 𝐹 ∘ 𝐺 ) ∈ ran ( 𝐹 ∘ 𝐺 ) )
40		rnco2	⊢ ran ( 𝐹 ∘ 𝐺 ) = ( 𝐹 “ ran 𝐺 )
41	40	inteqi	⊢ ∩ ran ( 𝐹 ∘ 𝐺 ) = ∩ ( 𝐹 “ ran 𝐺 )
42	39 41 40	3eltr3g	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ∩ ( 𝐹 “ ran 𝐺 ) ∈ ( 𝐹 “ ran 𝐺 ) )
43		fnfvima	⊢ ( ( 𝐹 Fn 𝒫 𝐴 ∧ ( 𝐹 “ ran 𝐺 ) ⊆ 𝒫 𝐴 ∧ ∩ ( 𝐹 “ ran 𝐺 ) ∈ ( 𝐹 “ ran 𝐺 ) ) → ( 𝐹 ‘ ∩ ( 𝐹 “ ran 𝐺 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) )
44	5 9 42 43	syl3anc	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ( 𝐹 ‘ ∩ ( 𝐹 “ ran 𝐺 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) )
45		simpl	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → 𝐴 ∈ Fin^III )
46	6 7	sstrid	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 “ ran 𝐺 ) ⊆ 𝒫 𝐴 )
47		incom	⊢ ( dom 𝐹 ∩ ran 𝐺 ) = ( ran 𝐺 ∩ dom 𝐹 )
48		frn	⊢ ( 𝐺 : ω ⟶ 𝒫 𝐴 → ran 𝐺 ⊆ 𝒫 𝐴 )
49	48	adantl	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ran 𝐺 ⊆ 𝒫 𝐴 )
50	3	fdmd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → dom 𝐹 = 𝒫 𝐴 )
51	49 50	sseqtrrd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ran 𝐺 ⊆ dom 𝐹 )
52		df-ss	⊢ ( ran 𝐺 ⊆ dom 𝐹 ↔ ( ran 𝐺 ∩ dom 𝐹 ) = ran 𝐺 )
53	51 52	sylib	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( ran 𝐺 ∩ dom 𝐹 ) = ran 𝐺 )
54	47 53	syl5eq	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( dom 𝐹 ∩ ran 𝐺 ) = ran 𝐺 )
55		fdm	⊢ ( 𝐺 : ω ⟶ 𝒫 𝐴 → dom 𝐺 = ω )
56	55	adantl	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → dom 𝐺 = ω )
57		peano1	⊢ ∅ ∈ ω
58		ne0i	⊢ ( ∅ ∈ ω → ω ≠ ∅ )
59	57 58	mp1i	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ω ≠ ∅ )
60	56 59	eqnetrd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → dom 𝐺 ≠ ∅ )
61		dm0rn0	⊢ ( dom 𝐺 = ∅ ↔ ran 𝐺 = ∅ )
62	61	necon3bii	⊢ ( dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅ )
63	60 62	sylib	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ran 𝐺 ≠ ∅ )
64	54 63	eqnetrd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( dom 𝐹 ∩ ran 𝐺 ) ≠ ∅ )
65		imadisj	⊢ ( ( 𝐹 “ ran 𝐺 ) = ∅ ↔ ( dom 𝐹 ∩ ran 𝐺 ) = ∅ )
66	65	necon3bii	⊢ ( ( 𝐹 “ ran 𝐺 ) ≠ ∅ ↔ ( dom 𝐹 ∩ ran 𝐺 ) ≠ ∅ )
67	64 66	sylibr	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 “ ran 𝐺 ) ≠ ∅ )
68	1	isf34lem5	⊢ ( ( 𝐴 ∈ Fin^III ∧ ( ( 𝐹 “ ran 𝐺 ) ⊆ 𝒫 𝐴 ∧ ( 𝐹 “ ran 𝐺 ) ≠ ∅ ) ) → ( 𝐹 ‘ ∩ ( 𝐹 “ ran 𝐺 ) ) = ∪ ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) )
69	45 46 67 68	syl12anc	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 ‘ ∩ ( 𝐹 “ ran 𝐺 ) ) = ∪ ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) )
70	1	isf34lem3	⊢ ( ( 𝐴 ∈ Fin^III ∧ ran 𝐺 ⊆ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) = ran 𝐺 )
71	45 49 70	syl2anc	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) = ran 𝐺 )
72	71	unieqd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ∪ ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) = ∪ ran 𝐺 )
73	69 72	eqtrd	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( 𝐹 ‘ ∩ ( 𝐹 “ ran 𝐺 ) ) = ∪ ran 𝐺 )
74	73 71	eleq12d	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ) → ( ( 𝐹 ‘ ∩ ( 𝐹 “ ran 𝐺 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) ↔ ∪ ran 𝐺 ∈ ran 𝐺 ) )
75	74	3adant3	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ( ( 𝐹 ‘ ∩ ( 𝐹 “ ran 𝐺 ) ) ∈ ( 𝐹 “ ( 𝐹 “ ran 𝐺 ) ) ↔ ∪ ran 𝐺 ∈ ran 𝐺 ) )
76	44 75	mpbid	⊢ ( ( 𝐴 ∈ Fin^III ∧ 𝐺 : ω ⟶ 𝒫 𝐴 ∧ ∀ 𝑦 ∈ ω ( 𝐺 ‘ 𝑦 ) ⊆ ( 𝐺 ‘ suc 𝑦 ) ) → ∪ ran 𝐺 ∈ ran 𝐺 )

Metamath Proof Explorer

Theorem isf34lem7

Proof