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

Theorem wunex2 10587
Description: Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wunex2.f 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)
wunex2.u 𝑈 = ran 𝐹
Assertion
Ref Expression
wunex2 (𝐴𝑉 → (𝑈 ∈ WUni ∧ 𝐴𝑈))
Distinct variable group:   𝑥,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧)   𝑈(𝑥,𝑦,𝑧)   𝐹(𝑥,𝑦,𝑧)   𝑉(𝑥,𝑦,𝑧)

Proof of Theorem wunex2
Dummy variables 𝑢 𝑎 𝑣 𝑤 𝑏 𝑚 𝑛 𝑖 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wunex2.u . . . . . . . 8 𝑈 = ran 𝐹
21eleq2i 2828 . . . . . . 7 (𝑎𝑈𝑎 ran 𝐹)
3 frfnom 8328 . . . . . . . . 9 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn ω
4 wunex2.f . . . . . . . . . 10 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)
54fneq1i 6576 . . . . . . . . 9 (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn ω)
63, 5mpbir 230 . . . . . . . 8 𝐹 Fn ω
7 fnunirn 7177 . . . . . . . 8 (𝐹 Fn ω → (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚)))
86, 7ax-mp 5 . . . . . . 7 (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
92, 8bitri 274 . . . . . 6 (𝑎𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
10 elssuni 4884 . . . . . . . . . . 11 (𝑎 ∈ (𝐹𝑚) → 𝑎 (𝐹𝑚))
1110ad2antll 726 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 (𝐹𝑚))
12 ssun2 4119 . . . . . . . . . . 11 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
13 ssun1 4118 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1412, 13sstri 3940 . . . . . . . . . 10 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1511, 14sstrdi 3943 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
16 simprl 768 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑚 ∈ ω)
17 fvex 6832 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1817uniex 7648 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1917, 18unex 7650 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ∈ V
20 prex 5374 . . . . . . . . . . . . 13 {𝒫 𝑢, 𝑢} ∈ V
2117mptex 7149 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2221rnex 7819 . . . . . . . . . . . . 13 ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2320, 22unex 7650 . . . . . . . . . . . 12 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2417, 23iunex 7871 . . . . . . . . . . 11 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2519, 24unex 7650 . . . . . . . . . 10 (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑧𝑤 = 𝑧)
27 unieq 4862 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑤 = 𝑧)
2826, 27uneq12d 4110 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (𝑤 𝑤) = (𝑧 𝑧))
29 pweq 4560 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30 unieq 4862 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 𝑢 = 𝑥)
3129, 30preq12d 4688 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → {𝒫 𝑢, 𝑢} = {𝒫 𝑥, 𝑥})
32 preq2 4681 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
3332cbvmptv 5202 . . . . . . . . . . . . . . . . 17 (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑢, 𝑦})
34 preq1 4680 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
3534mpteq2dv 5191 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → (𝑦𝑤 ↦ {𝑢, 𝑦}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3633, 35eqtrid 2788 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3736rneqd 5873 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
3831, 37uneq12d 4110 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})))
3938cbviunv 4984 . . . . . . . . . . . . 13 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
40 mpteq1 5182 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (𝑦𝑤 ↦ {𝑥, 𝑦}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
4140rneqd 5873 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → ran (𝑦𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦𝑧 ↦ {𝑥, 𝑦}))
4241uneq2d 4109 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4326, 42iuneq12d 4966 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4439, 43eqtrid 2788 . . . . . . . . . . . 12 (𝑤 = 𝑧 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4528, 44uneq12d 4110 . . . . . . . . . . 11 (𝑤 = 𝑧 → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦}))))
46 id 22 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
47 unieq 4862 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
4846, 47uneq12d 4110 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → (𝑤 𝑤) = ((𝐹𝑚) ∪ (𝐹𝑚)))
49 mpteq1 5182 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝑚) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5049rneqd 5873 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑚) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5150uneq2d 4109 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5246, 51iuneq12d 4966 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5348, 52uneq12d 4110 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
544, 45, 53frsucmpt2 8333 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5516, 25, 54sylancl 586 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5615, 55sseqtrrd 3972 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57 fvssunirn 6852 . . . . . . . . 9 (𝐹‘suc 𝑚) ⊆ ran 𝐹
5857, 1sseqtrri 3968 . . . . . . . 8 (𝐹‘suc 𝑚) ⊆ 𝑈
5956, 58sstrdi 3943 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
6059rexlimdvaa 3149 . . . . . 6 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → 𝑎𝑈))
619, 60biimtrid 241 . . . . 5 (𝐴𝑉 → (𝑎𝑈𝑎𝑈))
6261ralrimiv 3138 . . . 4 (𝐴𝑉 → ∀𝑎𝑈 𝑎𝑈)
63 dftr3 5212 . . . 4 (Tr 𝑈 ↔ ∀𝑎𝑈 𝑎𝑈)
6462, 63sylibr 233 . . 3 (𝐴𝑉 → Tr 𝑈)
65 1on 8371 . . . . . . . 8 1o ∈ On
66 unexg 7653 . . . . . . . 8 ((𝐴𝑉 ∧ 1o ∈ On) → (𝐴 ∪ 1o) ∈ V)
6765, 66mpan2 688 . . . . . . 7 (𝐴𝑉 → (𝐴 ∪ 1o) ∈ V)
684fveq1i 6820 . . . . . . . 8 (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)‘∅)
69 fr0g 8329 . . . . . . . 8 ((𝐴 ∪ 1o) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)‘∅) = (𝐴 ∪ 1o))
7068, 69eqtrid 2788 . . . . . . 7 ((𝐴 ∪ 1o) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1o))
7167, 70syl 17 . . . . . 6 (𝐴𝑉 → (𝐹‘∅) = (𝐴 ∪ 1o))
72 fvssunirn 6852 . . . . . . 7 (𝐹‘∅) ⊆ ran 𝐹
7372, 1sseqtrri 3968 . . . . . 6 (𝐹‘∅) ⊆ 𝑈
7471, 73eqsstrrdi 3986 . . . . 5 (𝐴𝑉 → (𝐴 ∪ 1o) ⊆ 𝑈)
7574unssbd 4134 . . . 4 (𝐴𝑉 → 1o𝑈)
76 1n0 8381 . . . 4 1o ≠ ∅
77 ssn0 4346 . . . 4 ((1o𝑈 ∧ 1o ≠ ∅) → 𝑈 ≠ ∅)
7875, 76, 77sylancl 586 . . 3 (𝐴𝑉𝑈 ≠ ∅)
79 pweq 4560 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80 unieq 4862 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 𝑢 = 𝑎)
8179, 80preq12d 4688 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → {𝒫 𝑢, 𝑢} = {𝒫 𝑎, 𝑎})
82 preq1 4680 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
8382mpteq2dv 5191 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8483rneqd 5873 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8581, 84uneq12d 4110 . . . . . . . . . . . . 13 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})))
8685ssiun2s 4992 . . . . . . . . . . . 12 (𝑎 ∈ (𝐹𝑚) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8786ad2antll 726 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
88 ssun2 4119 . . . . . . . . . . . . 13 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8988, 55sseqtrrid 3984 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
9089, 58sstrdi 3943 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
9187, 90sstrd 3941 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
9291unssad 4133 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → {𝒫 𝑎, 𝑎} ⊆ 𝑈)
93 vpwex 5317 . . . . . . . . . 10 𝒫 𝑎 ∈ V
94 vuniex 7646 . . . . . . . . . 10 𝑎 ∈ V
9593, 94prss 4766 . . . . . . . . 9 ((𝒫 𝑎𝑈 𝑎𝑈) ↔ {𝒫 𝑎, 𝑎} ⊆ 𝑈)
9692, 95sylibr 233 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝒫 𝑎𝑈 𝑎𝑈))
9796simprd 496 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
9896simpld 495 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝒫 𝑎𝑈)
991eleq2i 2828 . . . . . . . . . 10 (𝑏𝑈𝑏 ran 𝐹)
100 fnunirn 7177 . . . . . . . . . . 11 (𝐹 Fn ω → (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛)))
1016, 100ax-mp 5 . . . . . . . . . 10 (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
10299, 101bitri 274 . . . . . . . . 9 (𝑏𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
103 ordom 7782 . . . . . . . . . . . . . . . . 17 Ord ω
104 simplrl 774 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑚 ∈ ω)
105 simprl 768 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑛 ∈ ω)
106 ordunel 7732 . . . . . . . . . . . . . . . . 17 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
107103, 104, 105, 106mp3an2i 1465 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝑚𝑛) ∈ ω)
108 ssun1 4118 . . . . . . . . . . . . . . . . 17 𝑚 ⊆ (𝑚𝑛)
109 fveq2 6819 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
110109sseq2d 3963 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑚)))
111 fveq2 6819 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
112111sseq2d 3963 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑖)))
113 fveq2 6819 . . . . . . . . . . . . . . . . . . 19 (𝑘 = suc 𝑖 → (𝐹𝑘) = (𝐹‘suc 𝑖))
114113sseq2d 3963 . . . . . . . . . . . . . . . . . 18 (𝑘 = suc 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
115 fveq2 6819 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑚𝑛) → (𝐹𝑘) = (𝐹‘(𝑚𝑛)))
116115sseq2d 3963 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑚𝑛) → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛))))
117 ssidd 3954 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹𝑚))
118 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹𝑚) = (𝐹𝑖))
119 suceq 6361 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
120119fveq2d 6823 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
121118, 120sseq12d 3964 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹𝑖) ⊆ (𝐹‘suc 𝑖)))
122 ssun1 4118 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
123122, 13sstri 3940 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
12425, 54mpan2 688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
125123, 124sseqtrrid 3984 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹‘suc 𝑚))
126121, 125vtoclga 3522 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ω → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
127126ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
128 sstr2 3938 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) ⊆ (𝐹𝑖) → ((𝐹𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
129127, 128syl5com 31 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → ((𝐹𝑚) ⊆ (𝐹𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
130110, 112, 114, 116, 117, 129findsg 7806 . . . . . . . . . . . . . . . . 17 ((((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚𝑛)) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
131108, 130mpan2 688 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
132107, 104, 131syl2anc 584 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
133 simplrr 775 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹𝑚))
134132, 133sseldd 3932 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹‘(𝑚𝑛)))
13582mpteq2dv 5191 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
136135rneqd 5873 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
13781, 136uneq12d 4110 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})))
138137ssiun2s 4992 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐹‘(𝑚𝑛)) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
139134, 138syl 17 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
140 ssun2 4119 . . . . . . . . . . . . . . 15 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
141 fvex 6832 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
142141uniex 7648 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
143141, 142unex 7650 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∈ V
144141mptex 7149 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
145144rnex 7819 . . . . . . . . . . . . . . . . . . 19 ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
14620, 145unex 7650 . . . . . . . . . . . . . . . . . 18 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
147141, 146iunex 7871 . . . . . . . . . . . . . . . . 17 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
148143, 147unex 7650 . . . . . . . . . . . . . . . 16 (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
149 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
150 unieq 4862 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
151149, 150uneq12d 4110 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑤 𝑤) = ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))))
152 mpteq1 5182 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
153152rneqd 5873 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝐹‘(𝑚𝑛)) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
154153uneq2d 4109 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
155149, 154iuneq12d 4966 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
156151, 155uneq12d 4110 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹‘(𝑚𝑛)) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
1574, 45, 156frsucmpt2 8333 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
158107, 148, 157sylancl 586 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
159140, 158sseqtrrid 3984 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚𝑛)))
160 fvssunirn 6852 . . . . . . . . . . . . . . 15 (𝐹‘suc (𝑚𝑛)) ⊆ ran 𝐹
161160, 1sseqtrri 3968 . . . . . . . . . . . . . 14 (𝐹‘suc (𝑚𝑛)) ⊆ 𝑈
162159, 161sstrdi 3943 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
163139, 162sstrd 3941 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
164163unssbd 4134 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
165 ssun2 4119 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ (𝑚𝑛)
166 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑚𝑛) → 𝑖 = (𝑚𝑛))
167165, 166sseqtrrid 3984 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑚𝑛) → 𝑛𝑖)
168167biantrud 532 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛𝑖)))
169168bicomd 222 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝑛 ∈ ω ∧ 𝑛𝑖) ↔ 𝑛 ∈ ω))
170 fveq2 6819 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝐹𝑖) = (𝐹‘(𝑚𝑛)))
171170sseq2d 3963 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝐹𝑛) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
172169, 171imbi12d 344 . . . . . . . . . . . . . . 15 (𝑖 = (𝑚𝑛) → (((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)) ↔ (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))))
173 eleq1w 2819 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
174173anbi2d 629 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
175 sseq1 3956 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝑚𝑖𝑛𝑖))
176174, 175anbi12d 631 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖)))
177 fveq2 6819 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
178177sseq1d 3962 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → ((𝐹𝑚) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹𝑖)))
179176, 178imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))))
180110, 112, 114, 112, 117, 129findsg 7806 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖))
181179, 180chvarvv 2001 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))
182181expl 458 . . . . . . . . . . . . . . 15 (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)))
183172, 182vtoclga 3522 . . . . . . . . . . . . . 14 ((𝑚𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
184107, 105, 183sylc 65 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))
185 simprr 770 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹𝑛))
186184, 185sseldd 3932 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹‘(𝑚𝑛)))
187 prex 5374 . . . . . . . . . . . 12 {𝑎, 𝑏} ∈ V
188 eqid 2736 . . . . . . . . . . . . 13 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})
189 preq2 4681 . . . . . . . . . . . . 13 (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
190188, 189elrnmpt1s 5892 . . . . . . . . . . . 12 ((𝑏 ∈ (𝐹‘(𝑚𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
191186, 187, 190sylancl 586 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
192164, 191sseldd 3932 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
193192rexlimdvaa 3149 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛) → {𝑎, 𝑏} ∈ 𝑈))
194102, 193biimtrid 241 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝑏𝑈 → {𝑎, 𝑏} ∈ 𝑈))
195194ralrimiv 3138 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)
19697, 98, 1953jca 1127 . . . . . 6 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
197196rexlimdvaa 3149 . . . . 5 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
1989, 197biimtrid 241 . . . 4 (𝐴𝑉 → (𝑎𝑈 → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
199198ralrimiv 3138 . . 3 (𝐴𝑉 → ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
200 rdgfun 8309 . . . . . . . . 9 Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o))
201 omex 9492 . . . . . . . . 9 ω ∈ V
202 resfunexg 7141 . . . . . . . . 9 ((Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) ∈ V)
203200, 201, 202mp2an 689 . . . . . . . 8 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) ∈ V
2044, 203eqeltri 2833 . . . . . . 7 𝐹 ∈ V
205204rnex 7819 . . . . . 6 ran 𝐹 ∈ V
206205uniex 7648 . . . . 5 ran 𝐹 ∈ V
2071, 206eqeltri 2833 . . . 4 𝑈 ∈ V
208 iswun 10553 . . . 4 (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))))
209207, 208ax-mp 5 . . 3 (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
21064, 78, 199, 209syl3anbrc 1342 . 2 (𝐴𝑉𝑈 ∈ WUni)
21174unssad 4133 . 2 (𝐴𝑉𝐴𝑈)
212210, 211jca 512 1 (𝐴𝑉 → (𝑈 ∈ WUni ∧ 𝐴𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  Vcvv 3441  cun 3895  wss 3897  c0 4268  𝒫 cpw 4546  {cpr 4574   cuni 4851   ciun 4938  cmpt 5172  Tr wtr 5206  ran crn 5615  cres 5616  Ord word 6295  Oncon0 6296  suc csuc 6298  Fun wfun 6467   Fn wfn 6468  cfv 6473  ωcom 7772  reccrdg 8302  1oc1o 8352  WUnicwun 10549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-inf2 9490
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-ov 7332  df-om 7773  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-1o 8359  df-wun 10551
This theorem is referenced by:  wunex  10588  wuncval2  10596
  Copyright terms: Public domain W3C validator