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

Theorem isf34lem7 9844
 Description: Lemma for isfin3-4 9847. (Contributed by Stefan O'Rear, 7-Nov-2014.)
Hypothesis
Ref Expression
compss.a 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴𝑥))
Assertion
Ref Expression
isf34lem7 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → ran 𝐺 ∈ ran 𝐺)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐹   𝑦,𝐺
Allowed substitution hints:   𝐹(𝑥)   𝐺(𝑥)

Proof of Theorem isf34lem7
StepHypRef Expression
1 compss.a . . . . . . 7 𝐹 = (𝑥 ∈ 𝒫 𝐴 ↦ (𝐴𝑥))
21isf34lem2 9838 . . . . . 6 (𝐴 ∈ FinIII𝐹:𝒫 𝐴⟶𝒫 𝐴)
32adantr 484 . . . . 5 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
433adant3 1129 . . . 4 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → 𝐹:𝒫 𝐴⟶𝒫 𝐴)
54ffnd 6503 . . 3 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → 𝐹 Fn 𝒫 𝐴)
6 imassrn 5916 . . . 4 (𝐹 “ ran 𝐺) ⊆ ran 𝐹
73frnd 6509 . . . . 5 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → ran 𝐹 ⊆ 𝒫 𝐴)
873adant3 1129 . . . 4 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → ran 𝐹 ⊆ 𝒫 𝐴)
96, 8sstrid 3905 . . 3 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → (𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴)
10 simp1 1133 . . . . 5 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → 𝐴 ∈ FinIII)
11 fco 6520 . . . . . . 7 ((𝐹:𝒫 𝐴⟶𝒫 𝐴𝐺:ω⟶𝒫 𝐴) → (𝐹𝐺):ω⟶𝒫 𝐴)
122, 11sylan 583 . . . . . 6 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (𝐹𝐺):ω⟶𝒫 𝐴)
13123adant3 1129 . . . . 5 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → (𝐹𝐺):ω⟶𝒫 𝐴)
14 sscon 4046 . . . . . . . 8 ((𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → (𝐴 ∖ (𝐺‘suc 𝑦)) ⊆ (𝐴 ∖ (𝐺𝑦)))
15 simpr 488 . . . . . . . . . . 11 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → 𝐺:ω⟶𝒫 𝐴)
16 peano2 7606 . . . . . . . . . . 11 (𝑦 ∈ ω → suc 𝑦 ∈ ω)
17 fvco3 6755 . . . . . . . . . . 11 ((𝐺:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → ((𝐹𝐺)‘suc 𝑦) = (𝐹‘(𝐺‘suc 𝑦)))
1815, 16, 17syl2an 598 . . . . . . . . . 10 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹𝐺)‘suc 𝑦) = (𝐹‘(𝐺‘suc 𝑦)))
19 simpll 766 . . . . . . . . . . 11 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → 𝐴 ∈ FinIII)
20 ffvelrn 6845 . . . . . . . . . . . . 13 ((𝐺:ω⟶𝒫 𝐴 ∧ suc 𝑦 ∈ ω) → (𝐺‘suc 𝑦) ∈ 𝒫 𝐴)
2115, 16, 20syl2an 598 . . . . . . . . . . . 12 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺‘suc 𝑦) ∈ 𝒫 𝐴)
2221elpwid 4508 . . . . . . . . . . 11 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺‘suc 𝑦) ⊆ 𝐴)
231isf34lem1 9837 . . . . . . . . . . 11 ((𝐴 ∈ FinIII ∧ (𝐺‘suc 𝑦) ⊆ 𝐴) → (𝐹‘(𝐺‘suc 𝑦)) = (𝐴 ∖ (𝐺‘suc 𝑦)))
2419, 22, 23syl2anc 587 . . . . . . . . . 10 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐹‘(𝐺‘suc 𝑦)) = (𝐴 ∖ (𝐺‘suc 𝑦)))
2518, 24eqtrd 2793 . . . . . . . . 9 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹𝐺)‘suc 𝑦) = (𝐴 ∖ (𝐺‘suc 𝑦)))
26 fvco3 6755 . . . . . . . . . . 11 ((𝐺:ω⟶𝒫 𝐴𝑦 ∈ ω) → ((𝐹𝐺)‘𝑦) = (𝐹‘(𝐺𝑦)))
2726adantll 713 . . . . . . . . . 10 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹𝐺)‘𝑦) = (𝐹‘(𝐺𝑦)))
28 ffvelrn 6845 . . . . . . . . . . . . 13 ((𝐺:ω⟶𝒫 𝐴𝑦 ∈ ω) → (𝐺𝑦) ∈ 𝒫 𝐴)
2928adantll 713 . . . . . . . . . . . 12 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺𝑦) ∈ 𝒫 𝐴)
3029elpwid 4508 . . . . . . . . . . 11 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐺𝑦) ⊆ 𝐴)
311isf34lem1 9837 . . . . . . . . . . 11 ((𝐴 ∈ FinIII ∧ (𝐺𝑦) ⊆ 𝐴) → (𝐹‘(𝐺𝑦)) = (𝐴 ∖ (𝐺𝑦)))
3219, 30, 31syl2anc 587 . . . . . . . . . 10 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (𝐹‘(𝐺𝑦)) = (𝐴 ∖ (𝐺𝑦)))
3327, 32eqtrd 2793 . . . . . . . . 9 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐹𝐺)‘𝑦) = (𝐴 ∖ (𝐺𝑦)))
3425, 33sseq12d 3927 . . . . . . . 8 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → (((𝐹𝐺)‘suc 𝑦) ⊆ ((𝐹𝐺)‘𝑦) ↔ (𝐴 ∖ (𝐺‘suc 𝑦)) ⊆ (𝐴 ∖ (𝐺𝑦))))
3514, 34syl5ibr 249 . . . . . . 7 (((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) ∧ 𝑦 ∈ ω) → ((𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → ((𝐹𝐺)‘suc 𝑦) ⊆ ((𝐹𝐺)‘𝑦)))
3635ralimdva 3108 . . . . . 6 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦) → ∀𝑦 ∈ ω ((𝐹𝐺)‘suc 𝑦) ⊆ ((𝐹𝐺)‘𝑦)))
37363impia 1114 . . . . 5 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → ∀𝑦 ∈ ω ((𝐹𝐺)‘suc 𝑦) ⊆ ((𝐹𝐺)‘𝑦))
38 fin33i 9834 . . . . 5 ((𝐴 ∈ FinIII ∧ (𝐹𝐺):ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω ((𝐹𝐺)‘suc 𝑦) ⊆ ((𝐹𝐺)‘𝑦)) → ran (𝐹𝐺) ∈ ran (𝐹𝐺))
3910, 13, 37, 38syl3anc 1368 . . . 4 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → ran (𝐹𝐺) ∈ ran (𝐹𝐺))
40 rnco2 6087 . . . . 5 ran (𝐹𝐺) = (𝐹 “ ran 𝐺)
4140inteqi 4845 . . . 4 ran (𝐹𝐺) = (𝐹 “ ran 𝐺)
4239, 41, 403eltr3g 2868 . . 3 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → (𝐹 “ ran 𝐺) ∈ (𝐹 “ ran 𝐺))
43 fnfvima 6992 . . 3 ((𝐹 Fn 𝒫 𝐴 ∧ (𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴 (𝐹 “ ran 𝐺) ∈ (𝐹 “ ran 𝐺)) → (𝐹 (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)))
445, 9, 42, 43syl3anc 1368 . 2 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → (𝐹 (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)))
45 simpl 486 . . . . . 6 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → 𝐴 ∈ FinIII)
466, 7sstrid 3905 . . . . . 6 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴)
47 incom 4108 . . . . . . . . 9 (dom 𝐹 ∩ ran 𝐺) = (ran 𝐺 ∩ dom 𝐹)
48 frn 6508 . . . . . . . . . . . 12 (𝐺:ω⟶𝒫 𝐴 → ran 𝐺 ⊆ 𝒫 𝐴)
4948adantl 485 . . . . . . . . . . 11 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → ran 𝐺 ⊆ 𝒫 𝐴)
503fdmd 6512 . . . . . . . . . . 11 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → dom 𝐹 = 𝒫 𝐴)
5149, 50sseqtrrd 3935 . . . . . . . . . 10 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → ran 𝐺 ⊆ dom 𝐹)
52 df-ss 3877 . . . . . . . . . 10 (ran 𝐺 ⊆ dom 𝐹 ↔ (ran 𝐺 ∩ dom 𝐹) = ran 𝐺)
5351, 52sylib 221 . . . . . . . . 9 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (ran 𝐺 ∩ dom 𝐹) = ran 𝐺)
5447, 53syl5eq 2805 . . . . . . . 8 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (dom 𝐹 ∩ ran 𝐺) = ran 𝐺)
55 fdm 6510 . . . . . . . . . . 11 (𝐺:ω⟶𝒫 𝐴 → dom 𝐺 = ω)
5655adantl 485 . . . . . . . . . 10 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → dom 𝐺 = ω)
57 peano1 7605 . . . . . . . . . . 11 ∅ ∈ ω
58 ne0i 4235 . . . . . . . . . . 11 (∅ ∈ ω → ω ≠ ∅)
5957, 58mp1i 13 . . . . . . . . . 10 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → ω ≠ ∅)
6056, 59eqnetrd 3018 . . . . . . . . 9 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → dom 𝐺 ≠ ∅)
61 dm0rn0 5770 . . . . . . . . . 10 (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
6261necon3bii 3003 . . . . . . . . 9 (dom 𝐺 ≠ ∅ ↔ ran 𝐺 ≠ ∅)
6360, 62sylib 221 . . . . . . . 8 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → ran 𝐺 ≠ ∅)
6454, 63eqnetrd 3018 . . . . . . 7 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (dom 𝐹 ∩ ran 𝐺) ≠ ∅)
65 imadisj 5924 . . . . . . . 8 ((𝐹 “ ran 𝐺) = ∅ ↔ (dom 𝐹 ∩ ran 𝐺) = ∅)
6665necon3bii 3003 . . . . . . 7 ((𝐹 “ ran 𝐺) ≠ ∅ ↔ (dom 𝐹 ∩ ran 𝐺) ≠ ∅)
6764, 66sylibr 237 . . . . . 6 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (𝐹 “ ran 𝐺) ≠ ∅)
681isf34lem5 9843 . . . . . 6 ((𝐴 ∈ FinIII ∧ ((𝐹 “ ran 𝐺) ⊆ 𝒫 𝐴 ∧ (𝐹 “ ran 𝐺) ≠ ∅)) → (𝐹 (𝐹 “ ran 𝐺)) = (𝐹 “ (𝐹 “ ran 𝐺)))
6945, 46, 67, 68syl12anc 835 . . . . 5 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (𝐹 (𝐹 “ ran 𝐺)) = (𝐹 “ (𝐹 “ ran 𝐺)))
701isf34lem3 9840 . . . . . . 7 ((𝐴 ∈ FinIII ∧ ran 𝐺 ⊆ 𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝐺)) = ran 𝐺)
7145, 49, 70syl2anc 587 . . . . . 6 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝐺)) = ran 𝐺)
7271unieqd 4815 . . . . 5 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (𝐹 “ (𝐹 “ ran 𝐺)) = ran 𝐺)
7369, 72eqtrd 2793 . . . 4 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → (𝐹 (𝐹 “ ran 𝐺)) = ran 𝐺)
7473, 71eleq12d 2846 . . 3 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴) → ((𝐹 (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)) ↔ ran 𝐺 ∈ ran 𝐺))
75743adant3 1129 . 2 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → ((𝐹 (𝐹 “ ran 𝐺)) ∈ (𝐹 “ (𝐹 “ ran 𝐺)) ↔ ran 𝐺 ∈ ran 𝐺))
7644, 75mpbid 235 1 ((𝐴 ∈ FinIII𝐺:ω⟶𝒫 𝐴 ∧ ∀𝑦 ∈ ω (𝐺𝑦) ⊆ (𝐺‘suc 𝑦)) → ran 𝐺 ∈ ran 𝐺)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ∀wral 3070   ∖ cdif 3857   ∩ cin 3859   ⊆ wss 3860  ∅c0 4227  𝒫 cpw 4497  ∪ cuni 4801  ∩ cint 4841   ↦ cmpt 5115  dom cdm 5527  ran crn 5528   “ cima 5530   ∘ ccom 5531  suc csuc 6175   Fn wfn 6334  ⟶wf 6335  ‘cfv 6339  ωcom 7584  FinIIIcfin3 9746 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5159  ax-sep 5172  ax-nul 5179  ax-pow 5237  ax-pr 5301  ax-un 7464 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-pss 3879  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4842  df-iun 4888  df-br 5036  df-opab 5098  df-mpt 5116  df-tr 5142  df-id 5433  df-eprel 5438  df-po 5446  df-so 5447  df-fr 5486  df-se 5487  df-we 5488  df-xp 5533  df-rel 5534  df-cnv 5535  df-co 5536  df-dm 5537  df-rn 5538  df-res 5539  df-ima 5540  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7113  df-rpss 7452  df-om 7585  df-wrecs 7962  df-recs 8023  df-rdg 8061  df-1o 8117  df-er 8304  df-en 8533  df-dom 8534  df-sdom 8535  df-fin 8536  df-wdom 9067  df-card 9406  df-fin4 9752  df-fin3 9753 This theorem is referenced by:  isf34lem6  9845  fin34i  9846
 Copyright terms: Public domain W3C validator