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

Theorem wuncval2 9448
 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 (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)
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 (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)
2 wuncval2.u . . . 4 𝑈 = ran 𝐹
31, 2wunex2 9439 . . 3 (𝐴𝑉 → (𝑈 ∈ WUni ∧ 𝐴𝑈))
4 wuncss 9446 . . 3 ((𝑈 ∈ WUni ∧ 𝐴𝑈) → (wUniCl‘𝐴) ⊆ 𝑈)
53, 4syl 17 . 2 (𝐴𝑉 → (wUniCl‘𝐴) ⊆ 𝑈)
6 frfnom 7417 . . . . . 6 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω
71fneq1i 5899 . . . . . 6 (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω)
86, 7mpbir 220 . . . . 5 𝐹 Fn ω
9 fniunfv 6409 . . . . 5 (𝐹 Fn ω → 𝑚 ∈ ω (𝐹𝑚) = ran 𝐹)
108, 9ax-mp 5 . . . 4 𝑚 ∈ ω (𝐹𝑚) = ran 𝐹
112, 10eqtr4i 2635 . . 3 𝑈 = 𝑚 ∈ ω (𝐹𝑚)
12 fveq2 6103 . . . . . . . 8 (𝑚 = ∅ → (𝐹𝑚) = (𝐹‘∅))
1312sseq1d 3595 . . . . . . 7 (𝑚 = ∅ → ((𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘∅) ⊆ (wUniCl‘𝐴)))
14 fveq2 6103 . . . . . . . 8 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
1514sseq1d 3595 . . . . . . 7 (𝑚 = 𝑛 → ((𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹𝑛) ⊆ (wUniCl‘𝐴)))
16 fveq2 6103 . . . . . . . 8 (𝑚 = suc 𝑛 → (𝐹𝑚) = (𝐹‘suc 𝑛))
1716sseq1d 3595 . . . . . . 7 (𝑚 = suc 𝑛 → ((𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)))
18 1on 7454 . . . . . . . . . 10 1𝑜 ∈ On
19 unexg 6857 . . . . . . . . . 10 ((𝐴𝑉 ∧ 1𝑜 ∈ On) → (𝐴 ∪ 1𝑜) ∈ V)
2018, 19mpan2 703 . . . . . . . . 9 (𝐴𝑉 → (𝐴 ∪ 1𝑜) ∈ V)
211fveq1i 6104 . . . . . . . . . 10 (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅)
22 fr0g 7418 . . . . . . . . . 10 ((𝐴 ∪ 1𝑜) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅) = (𝐴 ∪ 1𝑜))
2321, 22syl5eq 2656 . . . . . . . . 9 ((𝐴 ∪ 1𝑜) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
2420, 23syl 17 . . . . . . . 8 (𝐴𝑉 → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
25 wuncid 9444 . . . . . . . . 9 (𝐴𝑉𝐴 ⊆ (wUniCl‘𝐴))
26 df1o2 7459 . . . . . . . . . 10 1𝑜 = {∅}
27 wunccl 9445 . . . . . . . . . . . 12 (𝐴𝑉 → (wUniCl‘𝐴) ∈ WUni)
2827wun0 9419 . . . . . . . . . . 11 (𝐴𝑉 → ∅ ∈ (wUniCl‘𝐴))
2928snssd 4281 . . . . . . . . . 10 (𝐴𝑉 → {∅} ⊆ (wUniCl‘𝐴))
3026, 29syl5eqss 3612 . . . . . . . . 9 (𝐴𝑉 → 1𝑜 ⊆ (wUniCl‘𝐴))
3125, 30unssd 3751 . . . . . . . 8 (𝐴𝑉 → (𝐴 ∪ 1𝑜) ⊆ (wUniCl‘𝐴))
3224, 31eqsstrd 3602 . . . . . . 7 (𝐴𝑉 → (𝐹‘∅) ⊆ (wUniCl‘𝐴))
33 simplr 788 . . . . . . . . . . 11 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → 𝑛 ∈ ω)
34 fvex 6113 . . . . . . . . . . . . 13 (𝐹𝑛) ∈ V
3534uniex 6851 . . . . . . . . . . . . 13 (𝐹𝑛) ∈ V
3634, 35unex 6854 . . . . . . . . . . . 12 ((𝐹𝑛) ∪ (𝐹𝑛)) ∈ V
37 prex 4836 . . . . . . . . . . . . . 14 {𝒫 𝑢, 𝑢} ∈ V
3834mptex 6390 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) ∈ V
3938rnex 6992 . . . . . . . . . . . . . 14 ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) ∈ V
4037, 39unex 6854 . . . . . . . . . . . . 13 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ∈ V
4134, 40iunex 7039 . . . . . . . . . . . 12 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ∈ V
4236, 41unex 6854 . . . . . . . . . . 11 (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))) ∈ V
43 id 22 . . . . . . . . . . . . . 14 (𝑤 = 𝑧𝑤 = 𝑧)
44 unieq 4380 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 𝑤 = 𝑧)
4543, 44uneq12d 3730 . . . . . . . . . . . . 13 (𝑤 = 𝑧 → (𝑤 𝑤) = (𝑧 𝑧))
46 pweq 4111 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
47 unieq 4380 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 𝑢 = 𝑥)
4846, 47preq12d 4220 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → {𝒫 𝑢, 𝑢} = {𝒫 𝑥, 𝑥})
49 preq1 4212 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → {𝑢, 𝑣} = {𝑥, 𝑣})
5049mpteq2dv 4673 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣𝑤 ↦ {𝑥, 𝑣}))
5150rneqd 5274 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣𝑤 ↦ {𝑥, 𝑣}))
5248, 51uneq12d 3730 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣})))
5352cbviunv 4495 . . . . . . . . . . . . . 14 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣}))
54 preq2 4213 . . . . . . . . . . . . . . . . . . 19 (𝑣 = 𝑦 → {𝑥, 𝑣} = {𝑥, 𝑦})
5554cbvmptv 4678 . . . . . . . . . . . . . . . . . 18 (𝑣𝑤 ↦ {𝑥, 𝑣}) = (𝑦𝑤 ↦ {𝑥, 𝑦})
56 mpteq1 4665 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑧 → (𝑦𝑤 ↦ {𝑥, 𝑦}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
5755, 56syl5eq 2656 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑧 → (𝑣𝑤 ↦ {𝑥, 𝑣}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
5857rneqd 5274 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → ran (𝑣𝑤 ↦ {𝑥, 𝑣}) = ran (𝑦𝑧 ↦ {𝑥, 𝑦}))
5958uneq2d 3729 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
6043, 59iuneq12d 4482 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑣𝑤 ↦ {𝑥, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
6153, 60syl5eq 2656 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
6245, 61uneq12d 3730 . . . . . . . . . . . 12 (𝑤 = 𝑧 → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦}))))
63 id 22 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑛) → 𝑤 = (𝐹𝑛))
64 unieq 4380 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑛) → 𝑤 = (𝐹𝑛))
6563, 64uneq12d 3730 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑛) → (𝑤 𝑤) = ((𝐹𝑛) ∪ (𝐹𝑛)))
66 mpteq1 4665 . . . . . . . . . . . . . . . 16 (𝑤 = (𝐹𝑛) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))
6766rneqd 5274 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝑛) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))
6867uneq2d 3729 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑛) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})))
6963, 68iuneq12d 4482 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑛) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})))
7065, 69uneq12d 3730 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑛) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))))
711, 62, 70frsucmpt2 7422 . . . . . . . . . . 11 ((𝑛 ∈ ω ∧ (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑛) = (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))))
7233, 42, 71sylancl 693 . . . . . . . . . 10 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) = (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))))
73 simpr 476 . . . . . . . . . . . 12 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹𝑛) ⊆ (wUniCl‘𝐴))
7427ad3antrrr 762 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → (wUniCl‘𝐴) ∈ WUni)
7573sselda 3568 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝑢 ∈ (wUniCl‘𝐴))
7674, 75wunelss 9409 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝑢 ⊆ (wUniCl‘𝐴))
7776ralrimiva 2949 . . . . . . . . . . . . 13 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹𝑛)𝑢 ⊆ (wUniCl‘𝐴))
78 unissb 4405 . . . . . . . . . . . . 13 ( (𝐹𝑛) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹𝑛)𝑢 ⊆ (wUniCl‘𝐴))
7977, 78sylibr 223 . . . . . . . . . . . 12 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹𝑛) ⊆ (wUniCl‘𝐴))
8073, 79unssd 3751 . . . . . . . . . . 11 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → ((𝐹𝑛) ∪ (𝐹𝑛)) ⊆ (wUniCl‘𝐴))
8174, 75wunpw 9408 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝒫 𝑢 ∈ (wUniCl‘𝐴))
8274, 75wununi 9407 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → 𝑢 ∈ (wUniCl‘𝐴))
83 prssi 4293 . . . . . . . . . . . . . . 15 ((𝒫 𝑢 ∈ (wUniCl‘𝐴) ∧ 𝑢 ∈ (wUniCl‘𝐴)) → {𝒫 𝑢, 𝑢} ⊆ (wUniCl‘𝐴))
8481, 82, 83syl2anc 691 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → {𝒫 𝑢, 𝑢} ⊆ (wUniCl‘𝐴))
8574adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → (wUniCl‘𝐴) ∈ WUni)
8675adantr 480 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → 𝑢 ∈ (wUniCl‘𝐴))
87 simplr 788 . . . . . . . . . . . . . . . . . 18 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → (𝐹𝑛) ⊆ (wUniCl‘𝐴))
8887sselda 3568 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → 𝑣 ∈ (wUniCl‘𝐴))
8985, 86, 88wunpr 9410 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) ∧ 𝑣 ∈ (𝐹𝑛)) → {𝑢, 𝑣} ∈ (wUniCl‘𝐴))
90 eqid 2610 . . . . . . . . . . . . . . . 16 (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})
9189, 90fmptd 6292 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}):(𝐹𝑛)⟶(wUniCl‘𝐴))
92 frn 5966 . . . . . . . . . . . . . . 15 ((𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}):(𝐹𝑛)⟶(wUniCl‘𝐴) → ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) ⊆ (wUniCl‘𝐴))
9391, 92syl 17 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}) ⊆ (wUniCl‘𝐴))
9484, 93unssd 3751 . . . . . . . . . . . . 13 ((((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹𝑛)) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
9594ralrimiva 2949 . . . . . . . . . . . 12 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
96 iunss 4497 . . . . . . . . . . . 12 ( 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
9795, 96sylibr 223 . . . . . . . . . . 11 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴))
9880, 97unssd 3751 . . . . . . . . . 10 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (((𝐹𝑛) ∪ (𝐹𝑛)) ∪ 𝑢 ∈ (𝐹𝑛)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑛) ↦ {𝑢, 𝑣}))) ⊆ (wUniCl‘𝐴))
9972, 98eqsstrd 3602 . . . . . . . . 9 (((𝐴𝑉𝑛 ∈ ω) ∧ (𝐹𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))
10099ex 449 . . . . . . . 8 ((𝐴𝑉𝑛 ∈ ω) → ((𝐹𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)))
101100expcom 450 . . . . . . 7 (𝑛 ∈ ω → (𝐴𝑉 → ((𝐹𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))))
10213, 15, 17, 32, 101finds2 6986 . . . . . 6 (𝑚 ∈ ω → (𝐴𝑉 → (𝐹𝑚) ⊆ (wUniCl‘𝐴)))
103102com12 32 . . . . 5 (𝐴𝑉 → (𝑚 ∈ ω → (𝐹𝑚) ⊆ (wUniCl‘𝐴)))
104103ralrimiv 2948 . . . 4 (𝐴𝑉 → ∀𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴))
105 iunss 4497 . . . 4 ( 𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴) ↔ ∀𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴))
106104, 105sylibr 223 . . 3 (𝐴𝑉 𝑚 ∈ ω (𝐹𝑚) ⊆ (wUniCl‘𝐴))
10711, 106syl5eqss 3612 . 2 (𝐴𝑉𝑈 ⊆ (wUniCl‘𝐴))
1085, 107eqssd 3585 1 (𝐴𝑉 → (wUniCl‘𝐴) = 𝑈)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  {cpr 4127  ∪ cuni 4372  ∪ ciun 4455   ↦ cmpt 4643  ran crn 5039   ↾ cres 5040  Oncon0 5640  suc csuc 5642   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  ωcom 6957  reccrdg 7392  1𝑜c1o 7440  WUnicwun 9401  wUniClcwunm 9402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-wun 9403  df-wunc 9404 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator