Metamath Proof Explorer

Theorem wuncval2

Description: Our earlier expression for a containing weak universe is in fact the weak universe closure. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses wuncval2.f ⊢ 𝐹 = ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω )
wuncval2.u ⊢ 𝑈 = ∪ ran 𝐹
Assertion wuncval2 ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) = 𝑈 )

Proof

Step Hyp Ref Expression
1 wuncval2.f ⊢ 𝐹 = ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω )
2 wuncval2.u ⊢ 𝑈 = ∪ ran 𝐹
3 1 2 wunex2 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈 ) )
4 wuncss ⊢ ( ( 𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈 ) → ( wUniCl ‘ 𝐴 ) ⊆ 𝑈 )
5 3 4 syl ⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) ⊆ 𝑈 )
6 frfnom ⊢ ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) Fn ω
7 1 fneq1i ⊢ ( 𝐹 Fn ω ↔ ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) Fn ω )
8 6 7 mpbir ⊢ 𝐹 Fn ω
9 fniunfv ⊢ ( 𝐹 Fn ω → ∪ 𝑚 ∈ ω ( 𝐹 ‘ 𝑚 ) = ∪ ran 𝐹 )
10 8 9 ax-mp ⊢ ∪ 𝑚 ∈ ω ( 𝐹 ‘ 𝑚 ) = ∪ ran 𝐹
11 2 10 eqtr4i ⊢ 𝑈 = ∪ 𝑚 ∈ ω ( 𝐹 ‘ 𝑚 )
12 fveq2 ⊢ ( 𝑚 = ∅ → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ ∅ ) )
13 12 sseq1d ⊢ ( 𝑚 = ∅ → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) ↔ ( 𝐹 ‘ ∅ ) ⊆ ( wUniCl ‘ 𝐴 ) ) )
14 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
15 14 sseq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) ↔ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) )
16 fveq2 ⊢ ( 𝑚 = suc 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ suc 𝑛 ) )
17 16 sseq1d ⊢ ( 𝑚 = suc 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) ↔ ( 𝐹 ‘ suc 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) )
18 1on ⊢ 1o ∈ On
19 unexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1o ∈ On ) → ( 𝐴 ∪ 1o ) ∈ V )
20 18 19 mpan2 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∪ 1o ) ∈ V )
21 1 fveq1i ⊢ ( 𝐹 ‘ ∅ ) = ( ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ‘ ∅ )
22 fr0g ⊢ ( ( 𝐴 ∪ 1o ) ∈ V → ( ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ‘ ∅ ) = ( 𝐴 ∪ 1o ) )
23 21 22 syl5eq ⊢ ( ( 𝐴 ∪ 1o ) ∈ V → ( 𝐹 ‘ ∅ ) = ( 𝐴 ∪ 1o ) )
24 20 23 syl ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ ∅ ) = ( 𝐴 ∪ 1o ) )
25 wuncid ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( wUniCl ‘ 𝐴 ) )
26 df1o2 ⊢ 1o = { ∅ }
27 wunccl ⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) ∈ WUni )
28 27 wun0 ⊢ ( 𝐴 ∈ 𝑉 → ∅ ∈ ( wUniCl ‘ 𝐴 ) )
29 28 snssd ⊢ ( 𝐴 ∈ 𝑉 → { ∅ } ⊆ ( wUniCl ‘ 𝐴 ) )
30 26 29 eqsstrid ⊢ ( 𝐴 ∈ 𝑉 → 1o ⊆ ( wUniCl ‘ 𝐴 ) )
31 25 30 unssd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∪ 1o ) ⊆ ( wUniCl ‘ 𝐴 ) )
32 24 31 eqsstrd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ ∅ ) ⊆ ( wUniCl ‘ 𝐴 ) )
33 simplr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → 𝑛 ∈ ω )
34 fvex ⊢ ( 𝐹 ‘ 𝑛 ) ∈ V
35 34 uniex ⊢ ∪ ( 𝐹 ‘ 𝑛 ) ∈ V
36 34 35 unex ⊢ ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ∈ V
37 prex ⊢ { 𝒫 𝑢 , ∪ 𝑢 } ∈ V
38 34 mptex ⊢ ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ∈ V
39 38 rnex ⊢ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ∈ V
40 37 39 unex ⊢ ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ∈ V
41 34 40 iunex ⊢ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ∈ V
42 36 41 unex ⊢ ( ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ) ∈ V
43 id ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
44 unieq ⊢ ( 𝑤 = 𝑧 → ∪ 𝑤 = ∪ 𝑧 )
45 43 44 uneq12d ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∪ ∪ 𝑤 ) = ( 𝑧 ∪ ∪ 𝑧 ) )
46 pweq ⊢ ( 𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥 )
47 unieq ⊢ ( 𝑢 = 𝑥 → ∪ 𝑢 = ∪ 𝑥 )
48 46 47 preq12d ⊢ ( 𝑢 = 𝑥 → { 𝒫 𝑢 , ∪ 𝑢 } = { 𝒫 𝑥 , ∪ 𝑥 } )
49 preq1 ⊢ ( 𝑢 = 𝑥 → { 𝑢 , 𝑣 } = { 𝑥 , 𝑣 } )
50 49 mpteq2dv ⊢ ( 𝑢 = 𝑥 → ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) )
51 50 rneqd ⊢ ( 𝑢 = 𝑥 → ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ran ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) )
52 48 51 uneq12d ⊢ ( 𝑢 = 𝑥 → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) ) )
53 52 cbviunv ⊢ ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ∪ 𝑥 ∈ 𝑤 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) )
54 preq2 ⊢ ( 𝑣 = 𝑦 → { 𝑥 , 𝑣 } = { 𝑥 , 𝑦 } )
55 54 cbvmptv ⊢ ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) = ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } )
56 mpteq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) = ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) )
57 55 56 syl5eq ⊢ ( 𝑤 = 𝑧 → ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) = ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) )
58 57 rneqd ⊢ ( 𝑤 = 𝑧 → ran ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) = ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) )
59 58 uneq2d ⊢ ( 𝑤 = 𝑧 → ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) ) = ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) )
60 43 59 iuneq12d ⊢ ( 𝑤 = 𝑧 → ∪ 𝑥 ∈ 𝑤 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑥 , 𝑣 } ) ) = ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) )
61 53 60 syl5eq ⊢ ( 𝑤 = 𝑧 → ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) )
62 45 61 uneq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∪ ∪ 𝑤 ) ∪ ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) ) = ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) )
63 id ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → 𝑤 = ( 𝐹 ‘ 𝑛 ) )
64 unieq ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → ∪ 𝑤 = ∪ ( 𝐹 ‘ 𝑛 ) )
65 63 64 uneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → ( 𝑤 ∪ ∪ 𝑤 ) = ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) )
66 mpteq1 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) )
67 66 rneqd ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) )
68 67 uneq2d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) )
69 63 68 iuneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) )
70 65 69 uneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑛 ) → ( ( 𝑤 ∪ ∪ 𝑤 ) ∪ ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
71 1 62 70 frsucmpt2 ⊢ ( ( 𝑛 ∈ ω ∧ ( ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ) ∈ V ) → ( 𝐹 ‘ suc 𝑛 ) = ( ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
72 33 42 71 sylancl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ( 𝐹 ‘ suc 𝑛 ) = ( ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
73 simpr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) )
74 27 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → ( wUniCl ‘ 𝐴 ) ∈ WUni )
75 73 sselda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑢 ∈ ( wUniCl ‘ 𝐴 ) )
76 74 75 wunelss ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑢 ⊆ ( wUniCl ‘ 𝐴 ) )
77 76 ralrimiva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ∀ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) 𝑢 ⊆ ( wUniCl ‘ 𝐴 ) )
78 unissb ⊢ ( ∪ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ↔ ∀ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) 𝑢 ⊆ ( wUniCl ‘ 𝐴 ) )
79 77 78 sylibr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ∪ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) )
80 73 79 unssd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
81 74 75 wunpw ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝒫 𝑢 ∈ ( wUniCl ‘ 𝐴 ) )
82 74 75 wununi ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → ∪ 𝑢 ∈ ( wUniCl ‘ 𝐴 ) )
83 81 82 prssd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → { 𝒫 𝑢 , ∪ 𝑢 } ⊆ ( wUniCl ‘ 𝐴 ) )
84 74 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ) → ( wUniCl ‘ 𝐴 ) ∈ WUni )
85 75 adantr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑢 ∈ ( wUniCl ‘ 𝐴 ) )
86 simplr ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) )
87 86 sselda ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ) → 𝑣 ∈ ( wUniCl ‘ 𝐴 ) )
88 84 85 87 wunpr ⊢ ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) ∧ 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ) → { 𝑢 , 𝑣 } ∈ ( wUniCl ‘ 𝐴 ) )
89 88 fmpttd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) : ( 𝐹 ‘ 𝑛 ) ⟶ ( wUniCl ‘ 𝐴 ) )
90 89 frnd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ⊆ ( wUniCl ‘ 𝐴 ) )
91 83 90 unssd ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ) → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
92 91 ralrimiva ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ∀ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
93 iunss ⊢ ( ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( wUniCl ‘ 𝐴 ) ↔ ∀ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
94 92 93 sylibr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
95 80 94 unssd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑛 ) ∪ ∪ ( 𝐹 ‘ 𝑛 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑛 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑛 ) ↦ { 𝑢 , 𝑣 } ) ) ) ⊆ ( wUniCl ‘ 𝐴 ) )
96 72 95 eqsstrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) ∧ ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) → ( 𝐹 ‘ suc 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) )
97 96 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω ) → ( ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) → ( 𝐹 ‘ suc 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) )
98 97 expcom ⊢ ( 𝑛 ∈ ω → ( 𝐴 ∈ 𝑉 → ( ( 𝐹 ‘ 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) → ( 𝐹 ‘ suc 𝑛 ) ⊆ ( wUniCl ‘ 𝐴 ) ) ) )
99 13 15 17 32 98 finds2 ⊢ ( 𝑚 ∈ ω → ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) ) )
100 99 com12 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑚 ∈ ω → ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) ) )
101 100 ralrimiv ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑚 ∈ ω ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) )
102 iunss ⊢ ( ∪ 𝑚 ∈ ω ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) ↔ ∀ 𝑚 ∈ ω ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) )
103 101 102 sylibr ⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝑚 ∈ ω ( 𝐹 ‘ 𝑚 ) ⊆ ( wUniCl ‘ 𝐴 ) )
104 11 103 eqsstrid ⊢ ( 𝐴 ∈ 𝑉 → 𝑈 ⊆ ( wUniCl ‘ 𝐴 ) )
105 5 104 eqssd ⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) = 𝑈 )