Metamath Proof Explorer

Theorem wunex2

Description: Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 wunex2.f ⊢ 𝐹 = ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω )
2 wunex2.u ⊢ 𝑈 = ∪ ran 𝐹
3 2 eleq2i ⊢ ( 𝑎 ∈ 𝑈 ↔ 𝑎 ∈ ∪ ran 𝐹 )
4 frfnom ⊢ ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) Fn ω
5 1 fneq1i ⊢ ( 𝐹 Fn ω ↔ ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) Fn ω )
6 4 5 mpbir ⊢ 𝐹 Fn ω
7 fnunirn ⊢ ( 𝐹 Fn ω → ( 𝑎 ∈ ∪ ran 𝐹 ↔ ∃ 𝑚 ∈ ω 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) )
8 6 7 ax-mp ⊢ ( 𝑎 ∈ ∪ ran 𝐹 ↔ ∃ 𝑚 ∈ ω 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) )
9 3 8 bitri ⊢ ( 𝑎 ∈ 𝑈 ↔ ∃ 𝑚 ∈ ω 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) )
10 elssuni ⊢ ( 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) → 𝑎 ⊆ ∪ ( 𝐹 ‘ 𝑚 ) )
11 10 ad2antll ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → 𝑎 ⊆ ∪ ( 𝐹 ‘ 𝑚 ) )
12 ssun2 ⊢ ∪ ( 𝐹 ‘ 𝑚 ) ⊆ ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) )
13 ssun1 ⊢ ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ⊆ ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
14 12 13 sstri ⊢ ∪ ( 𝐹 ‘ 𝑚 ) ⊆ ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
15 11 14 sstrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → 𝑎 ⊆ ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
16 simprl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → 𝑚 ∈ ω )
17 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
18 17 uniex ⊢ ∪ ( 𝐹 ‘ 𝑚 ) ∈ V
19 17 18 unex ⊢ ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∈ V
20 prex ⊢ { 𝒫 𝑢 , ∪ 𝑢 } ∈ V
21 17 mptex ⊢ ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ∈ V
22 21 rnex ⊢ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ∈ V
23 20 22 unex ⊢ ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ∈ V
24 17 23 iunex ⊢ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ∈ V
25 19 24 unex ⊢ ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ) ∈ V
26 id ⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
27 unieq ⊢ ( 𝑤 = 𝑧 → ∪ 𝑤 = ∪ 𝑧 )
28 26 27 uneq12d ⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∪ ∪ 𝑤 ) = ( 𝑧 ∪ ∪ 𝑧 ) )
29 pweq ⊢ ( 𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥 )
30 unieq ⊢ ( 𝑢 = 𝑥 → ∪ 𝑢 = ∪ 𝑥 )
31 29 30 preq12d ⊢ ( 𝑢 = 𝑥 → { 𝒫 𝑢 , ∪ 𝑢 } = { 𝒫 𝑥 , ∪ 𝑥 } )
32 preq2 ⊢ ( 𝑣 = 𝑦 → { 𝑢 , 𝑣 } = { 𝑢 , 𝑦 } )
33 32 cbvmptv ⊢ ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ( 𝑦 ∈ 𝑤 ↦ { 𝑢 , 𝑦 } )
34 preq1 ⊢ ( 𝑢 = 𝑥 → { 𝑢 , 𝑦 } = { 𝑥 , 𝑦 } )
35 34 mpteq2dv ⊢ ( 𝑢 = 𝑥 → ( 𝑦 ∈ 𝑤 ↦ { 𝑢 , 𝑦 } ) = ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) )
36 33 35 eqtrid ⊢ ( 𝑢 = 𝑥 → ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) )
37 36 rneqd ⊢ ( 𝑢 = 𝑥 → ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ran ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) )
38 31 37 uneq12d ⊢ ( 𝑢 = 𝑥 → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) ) )
39 38 cbviunv ⊢ ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ∪ 𝑥 ∈ 𝑤 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) )
40 mpteq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) = ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) )
41 40 rneqd ⊢ ( 𝑤 = 𝑧 → ran ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) = ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) )
42 41 uneq2d ⊢ ( 𝑤 = 𝑧 → ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) ) = ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) )
43 26 42 iuneq12d ⊢ ( 𝑤 = 𝑧 → ∪ 𝑥 ∈ 𝑤 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑤 ↦ { 𝑥 , 𝑦 } ) ) = ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) )
44 39 43 eqtrid ⊢ ( 𝑤 = 𝑧 → ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) )
45 28 44 uneq12d ⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∪ ∪ 𝑤 ) ∪ ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) ) = ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) )
46 id ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → 𝑤 = ( 𝐹 ‘ 𝑚 ) )
47 unieq ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ∪ 𝑤 = ∪ ( 𝐹 ‘ 𝑚 ) )
48 46 47 uneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ( 𝑤 ∪ ∪ 𝑤 ) = ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) )
49 mpteq1 ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) )
50 49 rneqd ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) )
51 50 uneq2d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
52 46 51 iuneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
53 48 52 uneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑚 ) → ( ( 𝑤 ∪ ∪ 𝑤 ) ∪ ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) ) = ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
54 1 45 53 frsucmpt2 ⊢ ( ( 𝑚 ∈ ω ∧ ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ) ∈ V ) → ( 𝐹 ‘ suc 𝑚 ) = ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
55 16 25 54 sylancl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝐹 ‘ suc 𝑚 ) = ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
56 15 55 sseqtrrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → 𝑎 ⊆ ( 𝐹 ‘ suc 𝑚 ) )
57 fvssunirn ⊢ ( 𝐹 ‘ suc 𝑚 ) ⊆ ∪ ran 𝐹
58 57 2 sseqtrri ⊢ ( 𝐹 ‘ suc 𝑚 ) ⊆ 𝑈
59 56 58 sstrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → 𝑎 ⊆ 𝑈 )
60 59 rexlimdvaa ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑚 ∈ ω 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) → 𝑎 ⊆ 𝑈 ) )
61 9 60 syl5bi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝑈 ) )
62 61 ralrimiv ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈 )
63 dftr3 ⊢ ( Tr 𝑈 ↔ ∀ 𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈 )
64 62 63 sylibr ⊢ ( 𝐴 ∈ 𝑉 → Tr 𝑈 )
65 1on ⊢ 1o ∈ On
66 unexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1o ∈ On ) → ( 𝐴 ∪ 1o ) ∈ V )
67 65 66 mpan2 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∪ 1o ) ∈ V )
68 1 fveq1i ⊢ ( 𝐹 ‘ ∅ ) = ( ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ‘ ∅ )
69 fr0g ⊢ ( ( 𝐴 ∪ 1o ) ∈ V → ( ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ‘ ∅ ) = ( 𝐴 ∪ 1o ) )
70 68 69 eqtrid ⊢ ( ( 𝐴 ∪ 1o ) ∈ V → ( 𝐹 ‘ ∅ ) = ( 𝐴 ∪ 1o ) )
71 67 70 syl ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ‘ ∅ ) = ( 𝐴 ∪ 1o ) )
72 fvssunirn ⊢ ( 𝐹 ‘ ∅ ) ⊆ ∪ ran 𝐹
73 72 2 sseqtrri ⊢ ( 𝐹 ‘ ∅ ) ⊆ 𝑈
74 71 73 eqsstrrdi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∪ 1o ) ⊆ 𝑈 )
75 74 unssbd ⊢ ( 𝐴 ∈ 𝑉 → 1o ⊆ 𝑈 )
76 1n0 ⊢ 1o ≠ ∅
77 ssn0 ⊢ ( ( 1o ⊆ 𝑈 ∧ 1o ≠ ∅ ) → 𝑈 ≠ ∅ )
78 75 76 77 sylancl ⊢ ( 𝐴 ∈ 𝑉 → 𝑈 ≠ ∅ )
79 pweq ⊢ ( 𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎 )
80 unieq ⊢ ( 𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎 )
81 79 80 preq12d ⊢ ( 𝑢 = 𝑎 → { 𝒫 𝑢 , ∪ 𝑢 } = { 𝒫 𝑎 , ∪ 𝑎 } )
82 preq1 ⊢ ( 𝑢 = 𝑎 → { 𝑢 , 𝑣 } = { 𝑎 , 𝑣 } )
83 82 mpteq2dv ⊢ ( 𝑢 = 𝑎 → ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) = ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑎 , 𝑣 } ) )
84 83 rneqd ⊢ ( 𝑢 = 𝑎 → ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) = ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑎 , 𝑣 } ) )
85 81 84 uneq12d ⊢ ( 𝑢 = 𝑎 → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) = ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑎 , 𝑣 } ) ) )
86 85 ssiun2s ⊢ ( 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) → ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑎 , 𝑣 } ) ) ⊆ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
87 86 ad2antll ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑎 , 𝑣 } ) ) ⊆ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
88 ssun2 ⊢ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
89 88 55 sseqtrrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( 𝐹 ‘ suc 𝑚 ) )
90 89 58 sstrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ 𝑈 )
91 87 90 sstrd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑎 , 𝑣 } ) ) ⊆ 𝑈 )
92 91 unssad ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → { 𝒫 𝑎 , ∪ 𝑎 } ⊆ 𝑈 )
93 vpwex ⊢ 𝒫 𝑎 ∈ V
94 vuniex ⊢ ∪ 𝑎 ∈ V
95 93 94 prss ⊢ ( ( 𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈 ) ↔ { 𝒫 𝑎 , ∪ 𝑎 } ⊆ 𝑈 )
96 92 95 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈 ) )
97 96 simprd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ∪ 𝑎 ∈ 𝑈 )
98 96 simpld ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → 𝒫 𝑎 ∈ 𝑈 )
99 2 eleq2i ⊢ ( 𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ ran 𝐹 )
100 fnunirn ⊢ ( 𝐹 Fn ω → ( 𝑏 ∈ ∪ ran 𝐹 ↔ ∃ 𝑛 ∈ ω 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) )
101 6 100 ax-mp ⊢ ( 𝑏 ∈ ∪ ran 𝐹 ↔ ∃ 𝑛 ∈ ω 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) )
102 99 101 bitri ⊢ ( 𝑏 ∈ 𝑈 ↔ ∃ 𝑛 ∈ ω 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) )
103 ordom ⊢ Ord ω
104 simplrl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → 𝑚 ∈ ω )
105 simprl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → 𝑛 ∈ ω )
106 ordunel ⊢ ( ( Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω ) → ( 𝑚 ∪ 𝑛 ) ∈ ω )
107 103 104 105 106 mp3an2i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝑚 ∪ 𝑛 ) ∈ ω )
108 ssun1 ⊢ 𝑚 ⊆ ( 𝑚 ∪ 𝑛 )
109 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
110 109 sseq2d ⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑚 ) ) )
111 fveq2 ⊢ ( 𝑘 = 𝑖 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑖 ) )
112 111 sseq2d ⊢ ( 𝑘 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑖 ) ) )
113 fveq2 ⊢ ( 𝑘 = suc 𝑖 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ suc 𝑖 ) )
114 113 sseq2d ⊢ ( 𝑘 = suc 𝑖 → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ suc 𝑖 ) ) )
115 fveq2 ⊢ ( 𝑘 = ( 𝑚 ∪ 𝑛 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
116 115 sseq2d ⊢ ( 𝑘 = ( 𝑚 ∪ 𝑛 ) → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) )
117 ssidd ⊢ ( 𝑚 ∈ ω → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑚 ) )
118 fveq2 ⊢ ( 𝑚 = 𝑖 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑖 ) )
119 suceq ⊢ ( 𝑚 = 𝑖 → suc 𝑚 = suc 𝑖 )
120 119 fveq2d ⊢ ( 𝑚 = 𝑖 → ( 𝐹 ‘ suc 𝑚 ) = ( 𝐹 ‘ suc 𝑖 ) )
121 118 120 sseq12d ⊢ ( 𝑚 = 𝑖 → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ suc 𝑚 ) ↔ ( 𝐹 ‘ 𝑖 ) ⊆ ( 𝐹 ‘ suc 𝑖 ) ) )
122 ssun1 ⊢ ( 𝐹 ‘ 𝑚 ) ⊆ ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) )
123 122 13 sstri ⊢ ( 𝐹 ‘ 𝑚 ) ⊆ ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) )
124 25 54 mpan2 ⊢ ( 𝑚 ∈ ω → ( 𝐹 ‘ suc 𝑚 ) = ( ( ( 𝐹 ‘ 𝑚 ) ∪ ∪ ( 𝐹 ‘ 𝑚 ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ 𝑚 ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ 𝑚 ) ↦ { 𝑢 , 𝑣 } ) ) ) )
125 123 124 sseqtrrid ⊢ ( 𝑚 ∈ ω → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ suc 𝑚 ) )
126 121 125 vtoclga ⊢ ( 𝑖 ∈ ω → ( 𝐹 ‘ 𝑖 ) ⊆ ( 𝐹 ‘ suc 𝑖 ) )
127 126 ad2antrr ⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑚 ∈ ω ) ∧ 𝑚 ⊆ 𝑖 ) → ( 𝐹 ‘ 𝑖 ) ⊆ ( 𝐹 ‘ suc 𝑖 ) )
128 sstr2 ⊢ ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑖 ) → ( ( 𝐹 ‘ 𝑖 ) ⊆ ( 𝐹 ‘ suc 𝑖 ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ suc 𝑖 ) ) )
129 127 128 syl5com ⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑚 ∈ ω ) ∧ 𝑚 ⊆ 𝑖 ) → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑖 ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ suc 𝑖 ) ) )
130 110 112 114 116 117 129 findsg ⊢ ( ( ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ 𝑚 ∈ ω ) ∧ 𝑚 ⊆ ( 𝑚 ∪ 𝑛 ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
131 108 130 mpan2 ⊢ ( ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ 𝑚 ∈ ω ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
132 107 104 131 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
133 simplrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) )
134 132 133 sseldd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → 𝑎 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
135 82 mpteq2dv ⊢ ( 𝑢 = 𝑎 → ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) = ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) )
136 135 rneqd ⊢ ( 𝑢 = 𝑎 → ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) = ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) )
137 81 136 uneq12d ⊢ ( 𝑢 = 𝑎 → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) = ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) ) )
138 137 ssiun2s ⊢ ( 𝑎 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) ) ⊆ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) )
139 134 138 syl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) ) ⊆ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) )
140 ssun2 ⊢ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) )
141 fvex ⊢ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∈ V
142 141 uniex ⊢ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∈ V
143 141 142 unex ⊢ ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ∈ V
144 141 mptex ⊢ ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ∈ V
145 144 rnex ⊢ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ∈ V
146 20 145 unex ⊢ ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ∈ V
147 141 146 iunex ⊢ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ∈ V
148 143 147 unex ⊢ ( ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ) ∈ V
149 id ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
150 unieq ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ∪ 𝑤 = ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
151 149 150 uneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ( 𝑤 ∪ ∪ 𝑤 ) = ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) )
152 mpteq1 ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) )
153 152 rneqd ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) = ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) )
154 153 uneq2d ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) )
155 149 154 iuneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) = ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) )
156 151 155 uneq12d ⊢ ( 𝑤 = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) → ( ( 𝑤 ∪ ∪ 𝑤 ) ∪ ∪ 𝑢 ∈ 𝑤 ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ 𝑤 ↦ { 𝑢 , 𝑣 } ) ) ) = ( ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ) )
157 1 45 156 frsucmpt2 ⊢ ( ( ( 𝑚 ∪ 𝑛 ) ∈ ω ∧ ( ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ) ∈ V ) → ( 𝐹 ‘ suc ( 𝑚 ∪ 𝑛 ) ) = ( ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ) )
158 107 148 157 sylancl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ suc ( 𝑚 ∪ 𝑛 ) ) = ( ( ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∪ ∪ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ∪ ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ) )
159 140 158 sseqtrrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ ( 𝐹 ‘ suc ( 𝑚 ∪ 𝑛 ) ) )
160 fvssunirn ⊢ ( 𝐹 ‘ suc ( 𝑚 ∪ 𝑛 ) ) ⊆ ∪ ran 𝐹
161 160 2 sseqtrri ⊢ ( 𝐹 ‘ suc ( 𝑚 ∪ 𝑛 ) ) ⊆ 𝑈
162 159 161 sstrdi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ∪ 𝑢 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ( { 𝒫 𝑢 , ∪ 𝑢 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑢 , 𝑣 } ) ) ⊆ 𝑈 )
163 139 162 sstrd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( { 𝒫 𝑎 , ∪ 𝑎 } ∪ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) ) ⊆ 𝑈 )
164 163 unssbd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) ⊆ 𝑈 )
165 ssun2 ⊢ 𝑛 ⊆ ( 𝑚 ∪ 𝑛 )
166 id ⊢ ( 𝑖 = ( 𝑚 ∪ 𝑛 ) → 𝑖 = ( 𝑚 ∪ 𝑛 ) )
167 165 166 sseqtrrid ⊢ ( 𝑖 = ( 𝑚 ∪ 𝑛 ) → 𝑛 ⊆ 𝑖 )
168 167 biantrud ⊢ ( 𝑖 = ( 𝑚 ∪ 𝑛 ) → ( 𝑛 ∈ ω ↔ ( 𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖 ) ) )
169 168 bicomd ⊢ ( 𝑖 = ( 𝑚 ∪ 𝑛 ) → ( ( 𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖 ) ↔ 𝑛 ∈ ω ) )
170 fveq2 ⊢ ( 𝑖 = ( 𝑚 ∪ 𝑛 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
171 170 sseq2d ⊢ ( 𝑖 = ( 𝑚 ∪ 𝑛 ) → ( ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑖 ) ↔ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) )
172 169 171 imbi12d ⊢ ( 𝑖 = ( 𝑚 ∪ 𝑛 ) → ( ( ( 𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖 ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑖 ) ) ↔ ( 𝑛 ∈ ω → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) ) )
173 eleq1w ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ∈ ω ↔ 𝑛 ∈ ω ) )
174 173 anbi2d ⊢ ( 𝑚 = 𝑛 → ( ( 𝑖 ∈ ω ∧ 𝑚 ∈ ω ) ↔ ( 𝑖 ∈ ω ∧ 𝑛 ∈ ω ) ) )
175 sseq1 ⊢ ( 𝑚 = 𝑛 → ( 𝑚 ⊆ 𝑖 ↔ 𝑛 ⊆ 𝑖 ) )
176 174 175 anbi12d ⊢ ( 𝑚 = 𝑛 → ( ( ( 𝑖 ∈ ω ∧ 𝑚 ∈ ω ) ∧ 𝑚 ⊆ 𝑖 ) ↔ ( ( 𝑖 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑛 ⊆ 𝑖 ) ) )
177 fveq2 ⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
178 177 sseq1d ⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑖 ) ↔ ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑖 ) ) )
179 176 178 imbi12d ⊢ ( 𝑚 = 𝑛 → ( ( ( ( 𝑖 ∈ ω ∧ 𝑚 ∈ ω ) ∧ 𝑚 ⊆ 𝑖 ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑖 ) ) ↔ ( ( ( 𝑖 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑛 ⊆ 𝑖 ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑖 ) ) ) )
180 110 112 114 112 117 129 findsg ⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑚 ∈ ω ) ∧ 𝑚 ⊆ 𝑖 ) → ( 𝐹 ‘ 𝑚 ) ⊆ ( 𝐹 ‘ 𝑖 ) )
181 179 180 chvarvv ⊢ ( ( ( 𝑖 ∈ ω ∧ 𝑛 ∈ ω ) ∧ 𝑛 ⊆ 𝑖 ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑖 ) )
182 181 expl ⊢ ( 𝑖 ∈ ω → ( ( 𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖 ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ 𝑖 ) ) )
183 172 182 vtoclga ⊢ ( ( 𝑚 ∪ 𝑛 ) ∈ ω → ( 𝑛 ∈ ω → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ) )
184 107 105 183 sylc ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → ( 𝐹 ‘ 𝑛 ) ⊆ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
185 simprr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) )
186 184 185 sseldd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → 𝑏 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) )
187 prex ⊢ { 𝑎 , 𝑏 } ∈ V
188 eqid ⊢ ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) = ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } )
189 preq2 ⊢ ( 𝑣 = 𝑏 → { 𝑎 , 𝑣 } = { 𝑎 , 𝑏 } )
190 188 189 elrnmpt1s ⊢ ( ( 𝑏 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ∧ { 𝑎 , 𝑏 } ∈ V ) → { 𝑎 , 𝑏 } ∈ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) )
191 186 187 190 sylancl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → { 𝑎 , 𝑏 } ∈ ran ( 𝑣 ∈ ( 𝐹 ‘ ( 𝑚 ∪ 𝑛 ) ) ↦ { 𝑎 , 𝑣 } ) )
192 164 191 sseldd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) ∧ ( 𝑛 ∈ ω ∧ 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) ) ) → { 𝑎 , 𝑏 } ∈ 𝑈 )
193 192 rexlimdvaa ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ( ∃ 𝑛 ∈ ω 𝑏 ∈ ( 𝐹 ‘ 𝑛 ) → { 𝑎 , 𝑏 } ∈ 𝑈 ) )
194 102 193 syl5bi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝑏 ∈ 𝑈 → { 𝑎 , 𝑏 } ∈ 𝑈 ) )
195 194 ralrimiv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ∀ 𝑏 ∈ 𝑈 { 𝑎 , 𝑏 } ∈ 𝑈 )
196 97 98 195 3jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑚 ∈ ω ∧ 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) ) ) → ( ∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀ 𝑏 ∈ 𝑈 { 𝑎 , 𝑏 } ∈ 𝑈 ) )
197 196 rexlimdvaa ⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑚 ∈ ω 𝑎 ∈ ( 𝐹 ‘ 𝑚 ) → ( ∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀ 𝑏 ∈ 𝑈 { 𝑎 , 𝑏 } ∈ 𝑈 ) ) )
198 9 197 syl5bi ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑎 ∈ 𝑈 → ( ∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀ 𝑏 ∈ 𝑈 { 𝑎 , 𝑏 } ∈ 𝑈 ) ) )
199 198 ralrimiv ⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑎 ∈ 𝑈 ( ∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀ 𝑏 ∈ 𝑈 { 𝑎 , 𝑏 } ∈ 𝑈 ) )
200 rdgfun ⊢ Fun rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) )
201 omex ⊢ ω ∈ V
202 resfunexg ⊢ ( ( Fun rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ∧ ω ∈ V ) → ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ∈ V )
203 200 201 202 mp2an ⊢ ( rec ( ( 𝑧 ∈ V ↦ ( ( 𝑧 ∪ ∪ 𝑧 ) ∪ ∪ 𝑥 ∈ 𝑧 ( { 𝒫 𝑥 , ∪ 𝑥 } ∪ ran ( 𝑦 ∈ 𝑧 ↦ { 𝑥 , 𝑦 } ) ) ) ) , ( 𝐴 ∪ 1o ) ) ↾ ω ) ∈ V
204 1 203 eqeltri ⊢ 𝐹 ∈ V
205 204 rnex ⊢ ran 𝐹 ∈ V
206 205 uniex ⊢ ∪ ran 𝐹 ∈ V
207 2 206 eqeltri ⊢ 𝑈 ∈ V
208 iswun ⊢ ( 𝑈 ∈ V → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝑈 ( ∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀ 𝑏 ∈ 𝑈 { 𝑎 , 𝑏 } ∈ 𝑈 ) ) ) )
209 207 208 ax-mp ⊢ ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑎 ∈ 𝑈 ( ∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀ 𝑏 ∈ 𝑈 { 𝑎 , 𝑏 } ∈ 𝑈 ) ) )
210 64 78 199 209 syl3anbrc ⊢ ( 𝐴 ∈ 𝑉 → 𝑈 ∈ WUni )
211 74 unssad ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈 )
212 210 211 jca ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈 ) )