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

Theorem wunex2 9439
 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 2680 . . . . . . 7 (𝑎𝑈𝑎 ran 𝐹)
3 frfnom 7417 . . . . . . . . 9 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω
4 wunex2.f . . . . . . . . . 10 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)
54fneq1i 5899 . . . . . . . . 9 (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) Fn ω)
63, 5mpbir 220 . . . . . . . 8 𝐹 Fn ω
7 fnunirn 6415 . . . . . . . 8 (𝐹 Fn ω → (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚)))
86, 7ax-mp 5 . . . . . . 7 (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
92, 8bitri 263 . . . . . 6 (𝑎𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
10 elssuni 4403 . . . . . . . . . . 11 (𝑎 ∈ (𝐹𝑚) → 𝑎 (𝐹𝑚))
1110ad2antll 761 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 (𝐹𝑚))
12 ssun2 3739 . . . . . . . . . . 11 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
13 ssun1 3738 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1412, 13sstri 3577 . . . . . . . . . 10 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1511, 14syl6ss 3580 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
16 simprl 790 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑚 ∈ ω)
17 fvex 6113 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1817uniex 6851 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1917, 18unex 6854 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ∈ V
20 prex 4836 . . . . . . . . . . . . 13 {𝒫 𝑢, 𝑢} ∈ V
2117mptex 6390 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2221rnex 6992 . . . . . . . . . . . . 13 ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2320, 22unex 6854 . . . . . . . . . . . 12 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2417, 23iunex 7039 . . . . . . . . . . 11 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2519, 24unex 6854 . . . . . . . . . 10 (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑧𝑤 = 𝑧)
27 unieq 4380 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑤 = 𝑧)
2826, 27uneq12d 3730 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (𝑤 𝑤) = (𝑧 𝑧))
29 pweq 4111 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30 unieq 4380 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 𝑢 = 𝑥)
3129, 30preq12d 4220 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → {𝒫 𝑢, 𝑢} = {𝒫 𝑥, 𝑥})
32 preq2 4213 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
3332cbvmptv 4678 . . . . . . . . . . . . . . . . 17 (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑢, 𝑦})
34 preq1 4212 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
3534mpteq2dv 4673 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → (𝑦𝑤 ↦ {𝑢, 𝑦}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3633, 35syl5eq 2656 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3736rneqd 5274 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
3831, 37uneq12d 3730 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})))
3938cbviunv 4495 . . . . . . . . . . . . 13 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
40 mpteq1 4665 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (𝑦𝑤 ↦ {𝑥, 𝑦}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
4140rneqd 5274 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → ran (𝑦𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦𝑧 ↦ {𝑥, 𝑦}))
4241uneq2d 3729 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4326, 42iuneq12d 4482 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4439, 43syl5eq 2656 . . . . . . . . . . . 12 (𝑤 = 𝑧 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4528, 44uneq12d 3730 . . . . . . . . . . 11 (𝑤 = 𝑧 → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦}))))
46 id 22 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
47 unieq 4380 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
4846, 47uneq12d 3730 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → (𝑤 𝑤) = ((𝐹𝑚) ∪ (𝐹𝑚)))
49 mpteq1 4665 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝑚) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5049rneqd 5274 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑚) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5150uneq2d 3729 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5246, 51iuneq12d 4482 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5348, 52uneq12d 3730 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
544, 45, 53frsucmpt2 7422 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5516, 25, 54sylancl 693 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5615, 55sseqtr4d 3605 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57 fvssunirn 6127 . . . . . . . . 9 (𝐹‘suc 𝑚) ⊆ ran 𝐹
5857, 1sseqtr4i 3601 . . . . . . . 8 (𝐹‘suc 𝑚) ⊆ 𝑈
5956, 58syl6ss 3580 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
6059rexlimdvaa 3014 . . . . . 6 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → 𝑎𝑈))
619, 60syl5bi 231 . . . . 5 (𝐴𝑉 → (𝑎𝑈𝑎𝑈))
6261ralrimiv 2948 . . . 4 (𝐴𝑉 → ∀𝑎𝑈 𝑎𝑈)
63 dftr3 4684 . . . 4 (Tr 𝑈 ↔ ∀𝑎𝑈 𝑎𝑈)
6462, 63sylibr 223 . . 3 (𝐴𝑉 → Tr 𝑈)
65 1on 7454 . . . . . . . 8 1𝑜 ∈ On
66 unexg 6857 . . . . . . . 8 ((𝐴𝑉 ∧ 1𝑜 ∈ On) → (𝐴 ∪ 1𝑜) ∈ V)
6765, 66mpan2 703 . . . . . . 7 (𝐴𝑉 → (𝐴 ∪ 1𝑜) ∈ V)
684fveq1i 6104 . . . . . . . 8 (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅)
69 fr0g 7418 . . . . . . . 8 ((𝐴 ∪ 1𝑜) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω)‘∅) = (𝐴 ∪ 1𝑜))
7068, 69syl5eq 2656 . . . . . . 7 ((𝐴 ∪ 1𝑜) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
7167, 70syl 17 . . . . . 6 (𝐴𝑉 → (𝐹‘∅) = (𝐴 ∪ 1𝑜))
72 fvssunirn 6127 . . . . . . 7 (𝐹‘∅) ⊆ ran 𝐹
7372, 1sseqtr4i 3601 . . . . . 6 (𝐹‘∅) ⊆ 𝑈
7471, 73syl6eqssr 3619 . . . . 5 (𝐴𝑉 → (𝐴 ∪ 1𝑜) ⊆ 𝑈)
7574unssbd 3753 . . . 4 (𝐴𝑉 → 1𝑜𝑈)
76 1n0 7462 . . . 4 1𝑜 ≠ ∅
77 ssn0 3928 . . . 4 ((1𝑜𝑈 ∧ 1𝑜 ≠ ∅) → 𝑈 ≠ ∅)
7875, 76, 77sylancl 693 . . 3 (𝐴𝑉𝑈 ≠ ∅)
79 pweq 4111 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80 unieq 4380 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 𝑢 = 𝑎)
8179, 80preq12d 4220 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → {𝒫 𝑢, 𝑢} = {𝒫 𝑎, 𝑎})
82 preq1 4212 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
8382mpteq2dv 4673 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8483rneqd 5274 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8581, 84uneq12d 3730 . . . . . . . . . . . . 13 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})))
8685ssiun2s 4500 . . . . . . . . . . . 12 (𝑎 ∈ (𝐹𝑚) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8786ad2antll 761 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
88 ssun2 3739 . . . . . . . . . . . . 13 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8988, 55syl5sseqr 3617 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
9089, 58syl6ss 3580 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
9187, 90sstrd 3578 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
9291unssad 3752 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → {𝒫 𝑎, 𝑎} ⊆ 𝑈)
93 vpwex 4775 . . . . . . . . . 10 𝒫 𝑎 ∈ V
94 vuniex 6852 . . . . . . . . . 10 𝑎 ∈ V
9593, 94prss 4291 . . . . . . . . 9 ((𝒫 𝑎𝑈 𝑎𝑈) ↔ {𝒫 𝑎, 𝑎} ⊆ 𝑈)
9692, 95sylibr 223 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝒫 𝑎𝑈 𝑎𝑈))
9796simprd 478 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
9896simpld 474 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝒫 𝑎𝑈)
991eleq2i 2680 . . . . . . . . . 10 (𝑏𝑈𝑏 ran 𝐹)
100 fnunirn 6415 . . . . . . . . . . 11 (𝐹 Fn ω → (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛)))
1016, 100ax-mp 5 . . . . . . . . . 10 (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
10299, 101bitri 263 . . . . . . . . 9 (𝑏𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
103 simplrl 796 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑚 ∈ ω)
104 simprl 790 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑛 ∈ ω)
105 ordom 6966 . . . . . . . . . . . . . . . . . 18 Ord ω
106 ordunel 6919 . . . . . . . . . . . . . . . . . 18 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
107105, 106mp3an1 1403 . . . . . . . . . . . . . . . . 17 ((𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
108103, 104, 107syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝑚𝑛) ∈ ω)
109 ssun1 3738 . . . . . . . . . . . . . . . . 17 𝑚 ⊆ (𝑚𝑛)
110 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
111110sseq2d 3596 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑚)))
112 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
113112sseq2d 3596 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑖)))
114 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = suc 𝑖 → (𝐹𝑘) = (𝐹‘suc 𝑖))
115114sseq2d 3596 . . . . . . . . . . . . . . . . . 18 (𝑘 = suc 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
116 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑚𝑛) → (𝐹𝑘) = (𝐹‘(𝑚𝑛)))
117116sseq2d 3596 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑚𝑛) → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛))))
118 ssid 3587 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑚) ⊆ (𝐹𝑚)
119118a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹𝑚))
120 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹𝑚) = (𝐹𝑖))
121 suceq 5707 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
122121fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
123120, 122sseq12d 3597 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹𝑖) ⊆ (𝐹‘suc 𝑖)))
124 ssun1 3738 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
125124, 13sstri 3577 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
12625, 54mpan2 703 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
127125, 126syl5sseqr 3617 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹‘suc 𝑚))
128123, 127vtoclga 3245 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ω → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
129128ad2antrr 758 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
130 sstr2 3575 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) ⊆ (𝐹𝑖) → ((𝐹𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
131129, 130syl5com 31 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → ((𝐹𝑚) ⊆ (𝐹𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
132111, 113, 115, 117, 119, 131findsg 6985 . . . . . . . . . . . . . . . . 17 ((((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚𝑛)) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
133109, 132mpan2 703 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
134108, 103, 133syl2anc 691 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
135 simplrr 797 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹𝑚))
136134, 135sseldd 3569 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹‘(𝑚𝑛)))
13782mpteq2dv 4673 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
138137rneqd 5274 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
13981, 138uneq12d 3730 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})))
140139ssiun2s 4500 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐹‘(𝑚𝑛)) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
141136, 140syl 17 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
142 ssun2 3739 . . . . . . . . . . . . . . 15 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
143 fvex 6113 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
144143uniex 6851 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
145143, 144unex 6854 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∈ V
146143mptex 6390 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
147146rnex 6992 . . . . . . . . . . . . . . . . . . 19 ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
14820, 147unex 6854 . . . . . . . . . . . . . . . . . 18 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
149143, 148iunex 7039 . . . . . . . . . . . . . . . . 17 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
150145, 149unex 6854 . . . . . . . . . . . . . . . 16 (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
151 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
152 unieq 4380 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
153151, 152uneq12d 3730 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑤 𝑤) = ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))))
154 mpteq1 4665 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
155154rneqd 5274 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝐹‘(𝑚𝑛)) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
156155uneq2d 3729 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
157151, 156iuneq12d 4482 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
158153, 157uneq12d 3730 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹‘(𝑚𝑛)) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
1594, 45, 158frsucmpt2 7422 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
160108, 150, 159sylancl 693 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
161142, 160syl5sseqr 3617 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚𝑛)))
162 fvssunirn 6127 . . . . . . . . . . . . . . 15 (𝐹‘suc (𝑚𝑛)) ⊆ ran 𝐹
163162, 1sseqtr4i 3601 . . . . . . . . . . . . . 14 (𝐹‘suc (𝑚𝑛)) ⊆ 𝑈
164161, 163syl6ss 3580 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
165141, 164sstrd 3578 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
166165unssbd 3753 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
167 ssun2 3739 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ (𝑚𝑛)
168 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑚𝑛) → 𝑖 = (𝑚𝑛))
169167, 168syl5sseqr 3617 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑚𝑛) → 𝑛𝑖)
170169biantrud 527 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛𝑖)))
171170bicomd 212 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝑛 ∈ ω ∧ 𝑛𝑖) ↔ 𝑛 ∈ ω))
172 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝐹𝑖) = (𝐹‘(𝑚𝑛)))
173172sseq2d 3596 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝐹𝑛) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
174171, 173imbi12d 333 . . . . . . . . . . . . . . 15 (𝑖 = (𝑚𝑛) → (((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)) ↔ (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))))
175 eleq1 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
176175anbi2d 736 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
177 sseq1 3589 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝑚𝑖𝑛𝑖))
178176, 177anbi12d 743 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖)))
179 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
180179sseq1d 3595 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → ((𝐹𝑚) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹𝑖)))
181178, 180imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))))
182111, 113, 115, 113, 119, 131findsg 6985 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖))
183181, 182chvarv 2251 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))
184183expl 646 . . . . . . . . . . . . . . 15 (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)))
185174, 184vtoclga 3245 . . . . . . . . . . . . . 14 ((𝑚𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
186108, 104, 185sylc 63 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))
187 simprr 792 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹𝑛))
188186, 187sseldd 3569 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹‘(𝑚𝑛)))
189 prex 4836 . . . . . . . . . . . 12 {𝑎, 𝑏} ∈ V
190 eqid 2610 . . . . . . . . . . . . 13 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})
191 preq2 4213 . . . . . . . . . . . . 13 (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
192190, 191elrnmpt1s 5294 . . . . . . . . . . . 12 ((𝑏 ∈ (𝐹‘(𝑚𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
193188, 189, 192sylancl 693 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
194166, 193sseldd 3569 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
195194rexlimdvaa 3014 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛) → {𝑎, 𝑏} ∈ 𝑈))
196102, 195syl5bi 231 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝑏𝑈 → {𝑎, 𝑏} ∈ 𝑈))
197196ralrimiv 2948 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)
19897, 98, 1973jca 1235 . . . . . 6 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
199198rexlimdvaa 3014 . . . . 5 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
2009, 199syl5bi 231 . . . 4 (𝐴𝑉 → (𝑎𝑈 → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
201200ralrimiv 2948 . . 3 (𝐴𝑉 → ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
202 rdgfun 7399 . . . . . . . . 9 Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜))
203 omex 8423 . . . . . . . . 9 ω ∈ V
204 resfunexg 6384 . . . . . . . . 9 ((Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) ∈ V)
205202, 203, 204mp2an 704 . . . . . . . 8 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾ ω) ∈ V
2064, 205eqeltri 2684 . . . . . . 7 𝐹 ∈ V
207206rnex 6992 . . . . . 6 ran 𝐹 ∈ V
208207uniex 6851 . . . . 5 ran 𝐹 ∈ V
2091, 208eqeltri 2684 . . . 4 𝑈 ∈ V
210 iswun 9405 . . . 4 (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))))
211209, 210ax-mp 5 . . 3 (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
21264, 78, 201, 211syl3anbrc 1239 . 2 (𝐴𝑉𝑈 ∈ WUni)
21374unssad 3752 . 2 (𝐴𝑉𝐴𝑈)
214212, 213jca 553 1 (𝐴𝑉 → (𝑈 ∈ WUni ∧ 𝐴𝑈))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {cpr 4127  ∪ cuni 4372  ∪ ciun 4455   ↦ cmpt 4643  Tr wtr 4680  ran crn 5039   ↾ cres 5040  Ord word 5639  Oncon0 5640  suc csuc 5642  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804  ωcom 6957  reccrdg 7392  1𝑜c1o 7440  WUnicwun 9401 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-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 This theorem is referenced by:  wunex  9440  wuncval2  9448
 Copyright terms: Public domain W3C validator