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

Theorem wuncval2 10787
Description: Our earlier expression for a containing weak universe is in fact the weak universe closure. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wuncval2.f 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)
wuncval2.u 𝑈 = ran 𝐹
Assertion
Ref Expression
wuncval2 (𝐴𝑉 → (wUniCl‘𝐴) = 𝑈)
Distinct variable groups:   𝑥,𝑦,𝑧   𝑥,𝐴,𝑦   𝑥,𝑉,𝑦
Allowed substitution hints:   𝐴(𝑧)   𝑈(𝑥,𝑦,𝑧)   𝐹(𝑥,𝑦,𝑧)   𝑉(𝑧)

Proof of Theorem wuncval2
Dummy variables 𝑣 𝑢 𝑤 𝑚 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wuncval2.f . . . 4 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)
2 wuncval2.u . . . 4 𝑈 = ran 𝐹
31, 2wunex2 10778 . . 3 (𝐴𝑉 → (𝑈 ∈ WUni ∧ 𝐴𝑈))
4 wuncss 10785 . . 3 ((𝑈 ∈ WUni ∧ 𝐴𝑈) → (wUniCl‘𝐴) ⊆ 𝑈)
53, 4syl 17 . 2 (𝐴𝑉 → (wUniCl‘𝐴) ⊆ 𝑈)
6 frfnom 8475 . . . . . 6 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn ω
71fneq1i 6665 . . . . . 6 (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn ω)
86, 7mpbir 231 . . . . 5 𝐹 Fn ω
9 fniunfv 7267 . . . . 5 (𝐹 Fn ω → 𝑚 ∈ ω (𝐹𝑚) = ran 𝐹)
108, 9ax-mp 5 . . . 4 𝑚 ∈ ω (𝐹𝑚) = ran 𝐹
112, 10eqtr4i 2768 . . 3 𝑈 = 𝑚 ∈ ω (𝐹𝑚)
12 fveq2 6906 . . . . . . . 8 (𝑚 = ∅ → (𝐹𝑚) = (𝐹‘∅))
1312sseq1d 4015 . . . . . . 7 (𝑚 = ∅ → ((𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘∅) ⊆ (wUniCl‘𝐴)))
14 fveq2 6906 . . . . . . . 8 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
1514sseq1d 4015 . . . . . . 7 (𝑚 = 𝑛 → ((𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹𝑛) ⊆ (wUniCl‘𝐴)))
16 fveq2 6906 . . . . . . . 8 (𝑚 = suc 𝑛 → (𝐹𝑚) = (𝐹‘suc 𝑛))
1716sseq1d 4015 . . . . . . 7 (𝑚 = suc 𝑛 → ((𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)))
18 1on 8518 . . . . . . . . . 10 1o ∈ On
19 unexg 7763 . . . . . . . . . 10 ((𝐴𝑉 ∧ 1o ∈ On) → (𝐴 ∪ 1o) ∈ V)
2018, 19mpan2 691 . . . . . . . . 9 (𝐴𝑉 → (𝐴 ∪ 1o) ∈ V)
211fveq1i 6907 . . . . . . . . . 10 (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)‘∅)
22 fr0g 8476 . . . . . . . . . 10 ((𝐴 ∪ 1o) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)‘∅) = (𝐴 ∪ 1o))
2321, 22eqtrid 2789 . . . . . . . . 9 ((𝐴 ∪ 1o) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1o))
2420, 23syl 17 . . . . . . . 8 (𝐴𝑉 → (𝐹‘∅) = (𝐴 ∪ 1o))
25 wuncid 10783 . . . . . . . . 9 (𝐴𝑉𝐴 ⊆ (wUniCl‘𝐴))
26 df1o2 8513 . . . . . . . . . 10 1o = {∅}
27 wunccl 10784 . . . . . . . . . . . 12 (𝐴𝑉 → (wUniCl‘𝐴) ∈ WUni)
2827wun0 10758 . . . . . . . . . . 11 (𝐴𝑉 → ∅ ∈ (wUniCl‘𝐴))
2928snssd 4809 . . . . . . . . . 10 (𝐴𝑉 → {∅} ⊆ (wUniCl‘𝐴))
3026, 29eqsstrid 4022 . . . . . . . . 9 (𝐴𝑉 → 1o ⊆ (wUniCl‘𝐴))
3125, 30unssd 4192 . . . . . . . 8 (𝐴𝑉 → (𝐴 ∪ 1o) ⊆ (wUniCl‘𝐴))
3224, 31eqsstrd 4018 . . . . . . 7 (𝐴𝑉 → (𝐹‘∅) ⊆ (wUniCl‘𝐴))
33 simplr 769 . . . . . . . . . . 11 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → 𝑛 ∈ ω)
34 fvex 6919 . . . . . . . . . . . . 13 (𝐹𝑛) ∈ V
3534uniex 7761 . . . . . . . . . . . . 13 (𝐹𝑛) ∈ V
3634, 35unex 7764 . . . . . . . . . . . 12 ((𝐹𝑛) ∪ (𝐹𝑛)) ∈ V
37 prex 5437 . . . . . . . . . . . . . 14 {𝒫 𝑢, 𝑢} ∈ V
3834mptex 7243 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) ∈ V
3938rnex 7932 . . . . . . . . . . . . . 14 ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) ∈ V
4037, 39unex 7764 . . . . . . . . . . . . 13 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ∈ V
4134, 40iunex 7993 . . . . . . . . . . . 12 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ∈ V
4236, 41unex 7764 . . . . . . . . . . 11 (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))) ∈ V
43 id 22 . . . . . . . . . . . . . 14 (𝑤 = 𝑧𝑤 = 𝑧)
44 unieq 4918 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 𝑤 = 𝑧)
4543, 44uneq12d 4169 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (𝑤 𝑤) = (𝑧 𝑧))
46 pweq 4614 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
47 unieq 4918 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 𝑢 = 𝑥)
4846, 47preq12d 4741 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → {𝒫 𝑢, 𝑢} = {𝒫 𝑥, 𝑥})
49 preq1 4733 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → {𝑢, 𝑣} = {𝑥, 𝑣})
5049mpteq2dv 5244 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣𝑤 ↦ {𝑥, 𝑣}))
5150rneqd 5949 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣𝑤 ↦ {𝑥, 𝑣}))
5248, 51uneq12d 4169 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣})))
5352cbviunv 5040 . . . . . . . . . . . . . 14 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣}))
54 preq2 4734 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑦 → {𝑥, 𝑣} = {𝑥, 𝑦})
5554cbvmptv 5255 . . . . . . . . . . . . . . . . . 18 (𝑣𝑤 ↦ {𝑥, 𝑣}) = (𝑦𝑤 ↦ {𝑥, 𝑦})
56 mpteq1 5235 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧 → (𝑦𝑤 ↦ {𝑥, 𝑦}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
5755, 56eqtrid 2789 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑧 → (𝑣𝑤 ↦ {𝑥, 𝑣}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
5857rneqd 5949 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → ran (𝑣𝑤 ↦ {𝑥, 𝑣}) = ran (𝑦𝑧 ↦ {𝑥, 𝑦}))
5958uneq2d 4168 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
6043, 59iuneq12d 5021 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
6153, 60eqtrid 2789 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
6245, 61uneq12d 4169 . . . . . . . . . . . 12 (𝑤 = 𝑧 → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦}))))
63 id 22 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑛) → 𝑤 = (𝐹𝑛))
64 unieq 4918 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑛) → 𝑤 = (𝐹𝑛))
6563, 64uneq12d 4169 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑛) → (𝑤 𝑤) = ((𝐹𝑛) ∪ (𝐹𝑛)))
66 mpteq1 5235 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐹𝑛) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))
6766rneqd 5949 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝑛) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))
6867uneq2d 4168 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑛) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})))
6963, 68iuneq12d 5021 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑛) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})))
7065, 69uneq12d 4169 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑛) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))))
711, 62, 70frsucmpt2 8480 . . . . . . . . . . 11 ((𝑛 ∈ ω ∧ (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑛) = (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))))
7233, 42, 71sylancl 586 . . . . . . . . . 10 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) = (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))))
73 simpr 484 . . . . . . . . . . . 12 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹𝑛) ⊆ (wUniCl‘𝐴))
7427ad3antrrr 730 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → (wUniCl‘𝐴) ∈ WUni)
7573sselda 3983 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝑢 ∈ (wUniCl‘𝐴))
7674, 75wunelss 10748 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝑢 ⊆ (wUniCl‘𝐴))
7776ralrimiva 3146 . . . . . . . . . . . . 13 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹𝑛)𝑢 ⊆ (wUniCl‘𝐴))
78 unissb 4939 . . . . . . . . . . . . 13 ( (𝐹𝑛) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹𝑛)𝑢 ⊆ (wUniCl‘𝐴))
7977, 78sylibr 234 . . . . . . . . . . . 12 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹𝑛) ⊆ (wUniCl‘𝐴))
8073, 79unssd 4192 . . . . . . . . . . 11 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → ((𝐹𝑛) ∪ (𝐹𝑛)) ⊆ (wUniCl‘𝐴))
8174, 75wunpw 10747 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝒫 𝑢 ∈ (wUniCl‘𝐴))
8274, 75wununi 10746 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝑢 ∈ (wUniCl‘𝐴))
8381, 82prssd 4822 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → {𝒫 𝑢, 𝑢} ⊆ (wUniCl‘𝐴))
8474adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → (wUniCl‘𝐴) ∈ WUni)
8575adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → 𝑢 ∈ (wUniCl‘𝐴))
86 simplr 769 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → (𝐹𝑛) ⊆ (wUniCl‘𝐴))
8786sselda 3983 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → 𝑣 ∈ (wUniCl‘𝐴))
8884, 85, 87wunpr 10749 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → {𝑢, 𝑣} ∈ (wUniCl‘𝐴))
8988fmpttd 7135 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}):(𝐹𝑛)⟶(wUniCl‘𝐴))
9089frnd 6744 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) ⊆ (wUniCl‘𝐴))
9183, 90unssd 4192 . . . . . . . . . . . . 13 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
9291ralrimiva 3146 . . . . . . . . . . . 12 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
93 iunss 5045 . . . . . . . . . . . 12 ( 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
9492, 93sylibr 234 . . . . . . . . . . 11 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
9580, 94unssd 4192 . . . . . . . . . 10 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))) ⊆ (wUniCl‘𝐴))
9672, 95eqsstrd 4018 . . . . . . . . 9 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))
9796ex 412 . . . . . . . 8 ((𝐴𝑉𝑛 ∈ ω) → ((𝐹𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)))
9897expcom 413 . . . . . . 7 (𝑛 ∈ ω → (𝐴𝑉 → ((𝐹𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))))
9913, 15, 17, 32, 98finds2 7920 . . . . . 6 (𝑚 ∈ ω → (𝐴𝑉 → (𝐹𝑚) ⊆ (wUniCl‘𝐴)))
10099com12 32 . . . . 5 (𝐴𝑉 → (𝑚 ∈ ω → (𝐹𝑚) ⊆ (wUniCl‘𝐴)))
101100ralrimiv 3145 . . . 4 (𝐴𝑉 → ∀𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴))
102 iunss 5045 . . . 4 ( 𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ ∀𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴))
103101, 102sylibr 234 . . 3 (𝐴𝑉 𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴))
10411, 103eqsstrid 4022 . 2 (𝐴𝑉𝑈 ⊆ (wUniCl‘𝐴))
1055, 104eqssd 4001 1 (𝐴𝑉 → (wUniCl‘𝐴) = 𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wral 3061  Vcvv 3480  cun 3949  wss 3951  c0 4333  𝒫 cpw 4600  {csn 4626  {cpr 4628   cuni 4907   ciun 4991  cmpt 5225  ran crn 5686  cres 5687  Oncon0 6384  suc csuc 6386   Fn wfn 6556  cfv 6561  ωcom 7887  reccrdg 8449  1oc1o 8499  WUnicwun 10740  wUniClcwunm 10741
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-wun 10742  df-wunc 10743
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator