This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isf34lem7

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

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

Proof

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