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

Theorem wunex2 9598
Description: Construct a weak universe from a given set. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wunex2.f 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)
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 2722 . . . . . . 7 (𝑎𝑈𝑎 ran 𝐹)
3 frfnom 7575 . . . . . . . . 9 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω
4 wunex2.f . . . . . . . . . 10 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)
54fneq1i 6023 . . . . . . . . 9 (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω)
63, 5mpbir 221 . . . . . . . 8 𝐹 Fn ω
7 fnunirn 6551 . . . . . . . 8 (𝐹 Fn ω → (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚)))
86, 7ax-mp 5 . . . . . . 7 (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
92, 8bitri 264 . . . . . 6 (𝑎𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
10 elssuni 4499 . . . . . . . . . . 11 (𝑎 ∈ (𝐹𝑚) → 𝑎 (𝐹𝑚))
1110ad2antll 765 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 (𝐹𝑚))
12 ssun2 3810 . . . . . . . . . . 11 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
13 ssun1 3809 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1412, 13sstri 3645 . . . . . . . . . 10 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1511, 14syl6ss 3648 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
16 simprl 809 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑚 ∈ ω)
17 fvex 6239 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1817uniex 6995 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1917, 18unex 6998 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ∈ V
20 prex 4939 . . . . . . . . . . . . 13 {𝒫 𝑢, 𝑢} ∈ V
2117mptex 6527 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2221rnex 7142 . . . . . . . . . . . . 13 ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2320, 22unex 6998 . . . . . . . . . . . 12 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2417, 23iunex 7189 . . . . . . . . . . 11 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2519, 24unex 6998 . . . . . . . . . 10 (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑧𝑤 = 𝑧)
27 unieq 4476 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑤 = 𝑧)
2826, 27uneq12d 3801 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (𝑤 𝑤) = (𝑧 𝑧))
29 pweq 4194 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30 unieq 4476 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 𝑢 = 𝑥)
3129, 30preq12d 4308 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → {𝒫 𝑢, 𝑢} = {𝒫 𝑥, 𝑥})
32 preq2 4301 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
3332cbvmptv 4783 . . . . . . . . . . . . . . . . 17 (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑢, 𝑦})
34 preq1 4300 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
3534mpteq2dv 4778 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → (𝑦𝑤 ↦ {𝑢, 𝑦}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3633, 35syl5eq 2697 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3736rneqd 5385 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
3831, 37uneq12d 3801 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})))
3938cbviunv 4591 . . . . . . . . . . . . 13 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
40 mpteq1 4770 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (𝑦𝑤 ↦ {𝑥, 𝑦}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
4140rneqd 5385 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → ran (𝑦𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦𝑧 ↦ {𝑥, 𝑦}))
4241uneq2d 3800 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4326, 42iuneq12d 4578 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4439, 43syl5eq 2697 . . . . . . . . . . . 12 (𝑤 = 𝑧 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4528, 44uneq12d 3801 . . . . . . . . . . 11 (𝑤 = 𝑧 → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦}))))
46 id 22 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
47 unieq 4476 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
4846, 47uneq12d 3801 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → (𝑤 𝑤) = ((𝐹𝑚) ∪ (𝐹𝑚)))
49 mpteq1 4770 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝑚) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5049rneqd 5385 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑚) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5150uneq2d 3800 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5246, 51iuneq12d 4578 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5348, 52uneq12d 3801 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
544, 45, 53frsucmpt2 7580 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5516, 25, 54sylancl 695 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5615, 55sseqtr4d 3675 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57 fvssunirn 6255 . . . . . . . . 9 (𝐹‘suc 𝑚) ⊆ ran 𝐹
5857, 1sseqtr4i 3671 . . . . . . . 8 (𝐹‘suc 𝑚) ⊆ 𝑈
5956, 58syl6ss 3648 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
6059rexlimdvaa 3061 . . . . . 6 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → 𝑎𝑈))
619, 60syl5bi 232 . . . . 5 (𝐴𝑉 → (𝑎𝑈𝑎𝑈))
6261ralrimiv 2994 . . . 4 (𝐴𝑉 → ∀𝑎𝑈 𝑎𝑈)
63 dftr3 4789 . . . 4 (Tr 𝑈 ↔ ∀𝑎𝑈 𝑎𝑈)
6462, 63sylibr 224 . . 3 (𝐴𝑉 → Tr 𝑈)
65 1on 7612 . . . . . . . 8 1𝑜 ∈ On
66 unexg 7001 . . . . . . . 8 ((𝐴𝑉 ∧ 1𝑜 ∈ On) → (𝐴 ∪ 1𝑜) ∈ V)
6765, 66mpan2 707 . . . . . . 7 (𝐴𝑉 → (𝐴 ∪ 1𝑜) ∈ V)
684fveq1i 6230 . . . . . . . 8 (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅)
69 fr0g 7576 . . . . . . . 8 ((𝐴 ∪ 1𝑜) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅) = (𝐴 ∪ 1𝑜))
7068, 69syl5eq 2697 . . . . . . 7 ((𝐴 ∪ 1𝑜) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
7167, 70syl 17 . . . . . 6 (𝐴𝑉 → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
72 fvssunirn 6255 . . . . . . 7 (𝐹‘∅) ⊆ ran 𝐹
7372, 1sseqtr4i 3671 . . . . . 6 (𝐹‘∅) ⊆ 𝑈
7471, 73syl6eqssr 3689 . . . . 5 (𝐴𝑉 → (𝐴 ∪ 1𝑜) ⊆ 𝑈)
7574unssbd 3824 . . . 4 (𝐴𝑉 → 1𝑜𝑈)
76 1n0 7620 . . . 4 1𝑜 ≠ ∅
77 ssn0 4009 . . . 4 ((1𝑜𝑈 ∧ 1𝑜 ≠ ∅) → 𝑈 ≠ ∅)
7875, 76, 77sylancl 695 . . 3 (𝐴𝑉𝑈 ≠ ∅)
79 pweq 4194 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80 unieq 4476 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 𝑢 = 𝑎)
8179, 80preq12d 4308 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → {𝒫 𝑢, 𝑢} = {𝒫 𝑎, 𝑎})
82 preq1 4300 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
8382mpteq2dv 4778 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8483rneqd 5385 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8581, 84uneq12d 3801 . . . . . . . . . . . . 13 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})))
8685ssiun2s 4596 . . . . . . . . . . . 12 (𝑎 ∈ (𝐹𝑚) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8786ad2antll 765 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
88 ssun2 3810 . . . . . . . . . . . . 13 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8988, 55syl5sseqr 3687 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
9089, 58syl6ss 3648 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
9187, 90sstrd 3646 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
9291unssad 3823 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → {𝒫 𝑎, 𝑎} ⊆ 𝑈)
93 vpwex 4879 . . . . . . . . . 10 𝒫 𝑎 ∈ V
94 vuniex 6996 . . . . . . . . . 10 𝑎 ∈ V
9593, 94prss 4383 . . . . . . . . 9 ((𝒫 𝑎𝑈 𝑎𝑈) ↔ {𝒫 𝑎, 𝑎} ⊆ 𝑈)
9692, 95sylibr 224 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝒫 𝑎𝑈 𝑎𝑈))
9796simprd 478 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
9896simpld 474 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝒫 𝑎𝑈)
991eleq2i 2722 . . . . . . . . . 10 (𝑏𝑈𝑏 ran 𝐹)
100 fnunirn 6551 . . . . . . . . . . 11 (𝐹 Fn ω → (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛)))
1016, 100ax-mp 5 . . . . . . . . . 10 (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
10299, 101bitri 264 . . . . . . . . 9 (𝑏𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
103 simplrl 817 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑚 ∈ ω)
104 simprl 809 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑛 ∈ ω)
105 ordom 7116 . . . . . . . . . . . . . . . . . 18 Ord ω
106 ordunel 7069 . . . . . . . . . . . . . . . . . 18 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
107105, 106mp3an1 1451 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
108103, 104, 107syl2anc 694 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝑚𝑛) ∈ ω)
109 ssun1 3809 . . . . . . . . . . . . . . . . 17 𝑚 ⊆ (𝑚𝑛)
110 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
111110sseq2d 3666 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑚)))
112 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
113112sseq2d 3666 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑖)))
114 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = suc 𝑖 → (𝐹𝑘) = (𝐹‘suc 𝑖))
115114sseq2d 3666 . . . . . . . . . . . . . . . . . 18 (𝑘 = suc 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
116 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑚𝑛) → (𝐹𝑘) = (𝐹‘(𝑚𝑛)))
117116sseq2d 3666 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑚𝑛) → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛))))
118 ssid 3657 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑚) ⊆ (𝐹𝑚)
119118a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹𝑚))
120 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹𝑚) = (𝐹𝑖))
121 suceq 5828 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
122121fveq2d 6233 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
123120, 122sseq12d 3667 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹𝑖) ⊆ (𝐹‘suc 𝑖)))
124 ssun1 3809 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
125124, 13sstri 3645 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
12625, 54mpan2 707 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
127125, 126syl5sseqr 3687 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹‘suc 𝑚))
128123, 127vtoclga 3303 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ω → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
129128ad2antrr 762 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
130 sstr2 3643 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) ⊆ (𝐹𝑖) → ((𝐹𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
131129, 130syl5com 31 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → ((𝐹𝑚) ⊆ (𝐹𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
132111, 113, 115, 117, 119, 131findsg 7135 . . . . . . . . . . . . . . . . 17 ((((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚𝑛)) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
133109, 132mpan2 707 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
134108, 103, 133syl2anc 694 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
135 simplrr 818 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹𝑚))
136134, 135sseldd 3637 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹‘(𝑚𝑛)))
13782mpteq2dv 4778 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
138137rneqd 5385 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
13981, 138uneq12d 3801 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})))
140139ssiun2s 4596 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐹‘(𝑚𝑛)) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
141136, 140syl 17 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
142 ssun2 3810 . . . . . . . . . . . . . . 15 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
143 fvex 6239 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
144143uniex 6995 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
145143, 144unex 6998 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∈ V
146143mptex 6527 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
147146rnex 7142 . . . . . . . . . . . . . . . . . . 19 ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
14820, 147unex 6998 . . . . . . . . . . . . . . . . . 18 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
149143, 148iunex 7189 . . . . . . . . . . . . . . . . 17 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
150145, 149unex 6998 . . . . . . . . . . . . . . . 16 (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
151 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
152 unieq 4476 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
153151, 152uneq12d 3801 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑤 𝑤) = ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))))
154 mpteq1 4770 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
155154rneqd 5385 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝐹‘(𝑚𝑛)) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
156155uneq2d 3800 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
157151, 156iuneq12d 4578 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
158153, 157uneq12d 3801 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹‘(𝑚𝑛)) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
1594, 45, 158frsucmpt2 7580 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
160108, 150, 159sylancl 695 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
161142, 160syl5sseqr 3687 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚𝑛)))
162 fvssunirn 6255 . . . . . . . . . . . . . . 15 (𝐹‘suc (𝑚𝑛)) ⊆ ran 𝐹
163162, 1sseqtr4i 3671 . . . . . . . . . . . . . 14 (𝐹‘suc (𝑚𝑛)) ⊆ 𝑈
164161, 163syl6ss 3648 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
165141, 164sstrd 3646 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
166165unssbd 3824 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
167 ssun2 3810 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ (𝑚𝑛)
168 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑚𝑛) → 𝑖 = (𝑚𝑛))
169167, 168syl5sseqr 3687 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑚𝑛) → 𝑛𝑖)
170169biantrud 527 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛𝑖)))
171170bicomd 213 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝑛 ∈ ω ∧ 𝑛𝑖) ↔ 𝑛 ∈ ω))
172 fveq2 6229 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝐹𝑖) = (𝐹‘(𝑚𝑛)))
173172sseq2d 3666 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝐹𝑛) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
174171, 173imbi12d 333 . . . . . . . . . . . . . . 15 (𝑖 = (𝑚𝑛) → (((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)) ↔ (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))))
175 eleq1 2718 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
176175anbi2d 740 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
177 sseq1 3659 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝑚𝑖𝑛𝑖))
178176, 177anbi12d 747 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖)))
179 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
180179sseq1d 3665 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → ((𝐹𝑚) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹𝑖)))
181178, 180imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))))
182111, 113, 115, 113, 119, 131findsg 7135 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖))
183181, 182chvarv 2299 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))
184183expl 647 . . . . . . . . . . . . . . 15 (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)))
185174, 184vtoclga 3303 . . . . . . . . . . . . . 14 ((𝑚𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
186108, 104, 185sylc 65 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))
187 simprr 811 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹𝑛))
188186, 187sseldd 3637 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹‘(𝑚𝑛)))
189 prex 4939 . . . . . . . . . . . 12 {𝑎, 𝑏} ∈ V
190 eqid 2651 . . . . . . . . . . . . 13 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})
191 preq2 4301 . . . . . . . . . . . . 13 (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
192190, 191elrnmpt1s 5405 . . . . . . . . . . . 12 ((𝑏 ∈ (𝐹‘(𝑚𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
193188, 189, 192sylancl 695 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
194166, 193sseldd 3637 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
195194rexlimdvaa 3061 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛) → {𝑎, 𝑏} ∈ 𝑈))
196102, 195syl5bi 232 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝑏𝑈 → {𝑎, 𝑏} ∈ 𝑈))
197196ralrimiv 2994 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)
19897, 98, 1973jca 1261 . . . . . 6 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
199198rexlimdvaa 3061 . . . . 5 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
2009, 199syl5bi 232 . . . 4 (𝐴𝑉 → (𝑎𝑈 → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
201200ralrimiv 2994 . . 3 (𝐴𝑉 → ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
202 rdgfun 7557 . . . . . . . . 9 Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜))
203 omex 8578 . . . . . . . . 9 ω ∈ V
204 resfunexg 6520 . . . . . . . . 9 ((Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) ∈ V)
205202, 203, 204mp2an 708 . . . . . . . 8 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) ∈ V
2064, 205eqeltri 2726 . . . . . . 7 𝐹 ∈ V
207206rnex 7142 . . . . . 6 ran 𝐹 ∈ V
208207uniex 6995 . . . . 5 ran 𝐹 ∈ V
2091, 208eqeltri 2726 . . . 4 𝑈 ∈ V
210 iswun 9564 . . . 4 (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))))
211209, 210ax-mp 5 . . 3 (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
21264, 78, 201, 211syl3anbrc 1265 . 2 (𝐴𝑉𝑈 ∈ WUni)
21374unssad 3823 . 2 (𝐴𝑉𝐴𝑈)
214212, 213jca 553 1 (𝐴𝑉 → (𝑈 ∈ WUni ∧ 𝐴𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  cun 3605  wss 3607  c0 3948  𝒫 cpw 4191  {cpr 4212   cuni 4468   ciun 4552  cmpt 4762  Tr wtr 4785  ran crn 5144  cres 5145  Ord word 5760  Oncon0 5761  suc csuc 5763  Fun wfun 5920   Fn wfn 5921  cfv 5926  ωcom 7107  reccrdg 7550  1𝑜c1o 7598  WUnicwun 9560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-om 7108  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-wun 9562
This theorem is referenced by:  wunex  9599  wuncval2  9607
  Copyright terms: Public domain W3C validator