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

Theorem wunex2 10153
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 2884 . . . . . . 7 (𝑎𝑈𝑎 ran 𝐹)
3 frfnom 8057 . . . . . . . . 9 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn ω
4 wunex2.f . . . . . . . . . 10 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)
54fneq1i 6424 . . . . . . . . 9 (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn ω)
63, 5mpbir 234 . . . . . . . 8 𝐹 Fn ω
7 fnunirn 6994 . . . . . . . 8 (𝐹 Fn ω → (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚)))
86, 7ax-mp 5 . . . . . . 7 (𝑎 ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
92, 8bitri 278 . . . . . 6 (𝑎𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚))
10 elssuni 4833 . . . . . . . . . . 11 (𝑎 ∈ (𝐹𝑚) → 𝑎 (𝐹𝑚))
1110ad2antll 728 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 (𝐹𝑚))
12 ssun2 4103 . . . . . . . . . . 11 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
13 ssun1 4102 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1412, 13sstri 3927 . . . . . . . . . 10 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
1511, 14sstrdi 3930 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
16 simprl 770 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑚 ∈ ω)
17 fvex 6662 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1817uniex 7451 . . . . . . . . . . . 12 (𝐹𝑚) ∈ V
1917, 18unex 7453 . . . . . . . . . . 11 ((𝐹𝑚) ∪ (𝐹𝑚)) ∈ V
20 prex 5301 . . . . . . . . . . . . 13 {𝒫 𝑢, 𝑢} ∈ V
2117mptex 6967 . . . . . . . . . . . . . 14 (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2221rnex 7603 . . . . . . . . . . . . 13 ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) ∈ V
2320, 22unex 7453 . . . . . . . . . . . 12 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2417, 23iunex 7655 . . . . . . . . . . 11 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ∈ V
2519, 24unex 7453 . . . . . . . . . 10 (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V
26 id 22 . . . . . . . . . . . . 13 (𝑤 = 𝑧𝑤 = 𝑧)
27 unieq 4814 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑤 = 𝑧)
2826, 27uneq12d 4094 . . . . . . . . . . . 12 (𝑤 = 𝑧 → (𝑤 𝑤) = (𝑧 𝑧))
29 pweq 4516 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥)
30 unieq 4814 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 𝑢 = 𝑥)
3129, 30preq12d 4640 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → {𝒫 𝑢, 𝑢} = {𝒫 𝑥, 𝑥})
32 preq2 4633 . . . . . . . . . . . . . . . . . 18 (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦})
3332cbvmptv 5136 . . . . . . . . . . . . . . . . 17 (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑢, 𝑦})
34 preq1 4632 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦})
3534mpteq2dv 5129 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑥 → (𝑦𝑤 ↦ {𝑢, 𝑦}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3633, 35syl5eq 2848 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥 → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑦𝑤 ↦ {𝑥, 𝑦}))
3736rneqd 5776 . . . . . . . . . . . . . . 15 (𝑢 = 𝑥 → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
3831, 37uneq12d 4094 . . . . . . . . . . . . . 14 (𝑢 = 𝑥 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})))
3938cbviunv 4930 . . . . . . . . . . . . 13 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦}))
40 mpteq1 5121 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑧 → (𝑦𝑤 ↦ {𝑥, 𝑦}) = (𝑦𝑧 ↦ {𝑥, 𝑦}))
4140rneqd 5776 . . . . . . . . . . . . . . 15 (𝑤 = 𝑧 → ran (𝑦𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦𝑧 ↦ {𝑥, 𝑦}))
4241uneq2d 4093 . . . . . . . . . . . . . 14 (𝑤 = 𝑧 → ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4326, 42iuneq12d 4912 . . . . . . . . . . . . 13 (𝑤 = 𝑧 𝑥𝑤 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑤 ↦ {𝑥, 𝑦})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4439, 43syl5eq 2848 . . . . . . . . . . . 12 (𝑤 = 𝑧 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))
4528, 44uneq12d 4094 . . . . . . . . . . 11 (𝑤 = 𝑧 → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦}))))
46 id 22 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
47 unieq 4814 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → 𝑤 = (𝐹𝑚))
4846, 47uneq12d 4094 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → (𝑤 𝑤) = ((𝐹𝑚) ∪ (𝐹𝑚)))
49 mpteq1 5121 . . . . . . . . . . . . . . 15 (𝑤 = (𝐹𝑚) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5049rneqd 5776 . . . . . . . . . . . . . 14 (𝑤 = (𝐹𝑚) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))
5150uneq2d 4093 . . . . . . . . . . . . 13 (𝑤 = (𝐹𝑚) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5246, 51iuneq12d 4912 . . . . . . . . . . . 12 (𝑤 = (𝐹𝑚) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
5348, 52uneq12d 4094 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
544, 45, 53frsucmpt2w 8062 . . . . . . . . . 10 ((𝑚 ∈ ω ∧ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5516, 25, 54sylancl 589 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
5615, 55sseqtrrd 3959 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚))
57 fvssunirn 6678 . . . . . . . . 9 (𝐹‘suc 𝑚) ⊆ ran 𝐹
5857, 1sseqtrri 3955 . . . . . . . 8 (𝐹‘suc 𝑚) ⊆ 𝑈
5956, 58sstrdi 3930 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
6059rexlimdvaa 3247 . . . . . 6 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → 𝑎𝑈))
619, 60syl5bi 245 . . . . 5 (𝐴𝑉 → (𝑎𝑈𝑎𝑈))
6261ralrimiv 3151 . . . 4 (𝐴𝑉 → ∀𝑎𝑈 𝑎𝑈)
63 dftr3 5143 . . . 4 (Tr 𝑈 ↔ ∀𝑎𝑈 𝑎𝑈)
6462, 63sylibr 237 . . 3 (𝐴𝑉 → Tr 𝑈)
65 1on 8096 . . . . . . . 8 1o ∈ On
66 unexg 7456 . . . . . . . 8 ((𝐴𝑉 ∧ 1o ∈ On) → (𝐴 ∪ 1o) ∈ V)
6765, 66mpan2 690 . . . . . . 7 (𝐴𝑉 → (𝐴 ∪ 1o) ∈ V)
684fveq1i 6650 . . . . . . . 8 (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)‘∅)
69 fr0g 8058 . . . . . . . 8 ((𝐴 ∪ 1o) ∈ V → ((rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)‘∅) = (𝐴 ∪ 1o))
7068, 69syl5eq 2848 . . . . . . 7 ((𝐴 ∪ 1o) ∈ V → (𝐹‘∅) = (𝐴 ∪ 1o))
7167, 70syl 17 . . . . . 6 (𝐴𝑉 → (𝐹‘∅) = (𝐴 ∪ 1o))
72 fvssunirn 6678 . . . . . . 7 (𝐹‘∅) ⊆ ran 𝐹
7372, 1sseqtrri 3955 . . . . . 6 (𝐹‘∅) ⊆ 𝑈
7471, 73eqsstrrdi 3973 . . . . 5 (𝐴𝑉 → (𝐴 ∪ 1o) ⊆ 𝑈)
7574unssbd 4118 . . . 4 (𝐴𝑉 → 1o𝑈)
76 1n0 8106 . . . 4 1o ≠ ∅
77 ssn0 4311 . . . 4 ((1o𝑈 ∧ 1o ≠ ∅) → 𝑈 ≠ ∅)
7875, 76, 77sylancl 589 . . 3 (𝐴𝑉𝑈 ≠ ∅)
79 pweq 4516 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎)
80 unieq 4814 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 𝑢 = 𝑎)
8179, 80preq12d 4640 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → {𝒫 𝑢, 𝑢} = {𝒫 𝑎, 𝑎})
82 preq1 4632 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣})
8382mpteq2dv 5129 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8483rneqd 5776 . . . . . . . . . . . . . 14 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣}))
8581, 84uneq12d 4094 . . . . . . . . . . . . 13 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})))
8685ssiun2s 4938 . . . . . . . . . . . 12 (𝑎 ∈ (𝐹𝑚) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8786ad2antll 728 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
88 ssun2 4103 . . . . . . . . . . . . 13 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
8988, 55sseqtrrid 3971 . . . . . . . . . . . 12 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚))
9089, 58sstrdi 3930 . . . . . . . . . . 11 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
9187, 90sstrd 3928 . . . . . . . . . 10 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
9291unssad 4117 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → {𝒫 𝑎, 𝑎} ⊆ 𝑈)
93 vpwex 5246 . . . . . . . . . 10 𝒫 𝑎 ∈ V
94 vuniex 7449 . . . . . . . . . 10 𝑎 ∈ V
9593, 94prss 4716 . . . . . . . . 9 ((𝒫 𝑎𝑈 𝑎𝑈) ↔ {𝒫 𝑎, 𝑎} ⊆ 𝑈)
9692, 95sylibr 237 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝒫 𝑎𝑈 𝑎𝑈))
9796simprd 499 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝑎𝑈)
9896simpld 498 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → 𝒫 𝑎𝑈)
991eleq2i 2884 . . . . . . . . . 10 (𝑏𝑈𝑏 ran 𝐹)
100 fnunirn 6994 . . . . . . . . . . 11 (𝐹 Fn ω → (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛)))
1016, 100ax-mp 5 . . . . . . . . . 10 (𝑏 ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
10299, 101bitri 278 . . . . . . . . 9 (𝑏𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛))
103 ordom 7573 . . . . . . . . . . . . . . . . 17 Ord ω
104 simplrl 776 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑚 ∈ ω)
105 simprl 770 . . . . . . . . . . . . . . . . 17 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑛 ∈ ω)
106 ordunel 7526 . . . . . . . . . . . . . . . . 17 ((Ord ω ∧ 𝑚 ∈ ω ∧ 𝑛 ∈ ω) → (𝑚𝑛) ∈ ω)
107103, 104, 105, 106mp3an2i 1463 . . . . . . . . . . . . . . . 16 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝑚𝑛) ∈ ω)
108 ssun1 4102 . . . . . . . . . . . . . . . . 17 𝑚 ⊆ (𝑚𝑛)
109 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑚 → (𝐹𝑘) = (𝐹𝑚))
110109sseq2d 3950 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑚 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑚)))
111 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝐹𝑘) = (𝐹𝑖))
112111sseq2d 3950 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹𝑖)))
113 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑘 = suc 𝑖 → (𝐹𝑘) = (𝐹‘suc 𝑖))
114113sseq2d 3950 . . . . . . . . . . . . . . . . . 18 (𝑘 = suc 𝑖 → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
115 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑘 = (𝑚𝑛) → (𝐹𝑘) = (𝐹‘(𝑚𝑛)))
116115sseq2d 3950 . . . . . . . . . . . . . . . . . 18 (𝑘 = (𝑚𝑛) → ((𝐹𝑚) ⊆ (𝐹𝑘) ↔ (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛))))
117 ssidd 3941 . . . . . . . . . . . . . . . . . 18 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹𝑚))
118 fveq2 6649 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹𝑚) = (𝐹𝑖))
119 suceq 6228 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖)
120119fveq2d 6653 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖))
121118, 120sseq12d 3951 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 = 𝑖 → ((𝐹𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹𝑖) ⊆ (𝐹‘suc 𝑖)))
122 ssun1 4102 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹𝑚) ⊆ ((𝐹𝑚) ∪ (𝐹𝑚))
123122, 13sstri 3927 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹𝑚) ⊆ (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣})))
12425, 54mpan2 690 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹𝑚) ∪ (𝐹𝑚)) ∪ 𝑢 ∈ (𝐹𝑚)({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹𝑚) ↦ {𝑢, 𝑣}))))
125123, 124sseqtrrid 3971 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ω → (𝐹𝑚) ⊆ (𝐹‘suc 𝑚))
126121, 125vtoclga 3525 . . . . . . . . . . . . . . . . . . . 20 (𝑖 ∈ ω → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
127126ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑖) ⊆ (𝐹‘suc 𝑖))
128 sstr2 3925 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑚) ⊆ (𝐹𝑖) → ((𝐹𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
129127, 128syl5com 31 . . . . . . . . . . . . . . . . . 18 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → ((𝐹𝑚) ⊆ (𝐹𝑖) → (𝐹𝑚) ⊆ (𝐹‘suc 𝑖)))
130110, 112, 114, 116, 117, 129findsg 7594 . . . . . . . . . . . . . . . . 17 ((((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚𝑛)) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
131108, 130mpan2 690 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
132107, 104, 131syl2anc 587 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑚) ⊆ (𝐹‘(𝑚𝑛)))
133 simplrr 777 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹𝑚))
134132, 133sseldd 3919 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑎 ∈ (𝐹‘(𝑚𝑛)))
13582mpteq2dv 5129 . . . . . . . . . . . . . . . . 17 (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
136135rneqd 5776 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
13781, 136uneq12d 4094 . . . . . . . . . . . . . . 15 (𝑢 = 𝑎 → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})))
138137ssiun2s 4938 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝐹‘(𝑚𝑛)) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
139134, 138syl 17 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
140 ssun2 4103 . . . . . . . . . . . . . . 15 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
141 fvex 6662 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
142141uniex 7451 . . . . . . . . . . . . . . . . . 18 (𝐹‘(𝑚𝑛)) ∈ V
143141, 142unex 7453 . . . . . . . . . . . . . . . . 17 ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∈ V
144141mptex 6967 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
145144rnex 7603 . . . . . . . . . . . . . . . . . . 19 ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}) ∈ V
14620, 145unex 7453 . . . . . . . . . . . . . . . . . 18 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
147141, 146iunex 7655 . . . . . . . . . . . . . . . . 17 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ∈ V
148143, 147unex 7453 . . . . . . . . . . . . . . . 16 (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V
149 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
150 unieq 4814 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑤 = (𝐹‘(𝑚𝑛)))
151149, 150uneq12d 4094 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑤 𝑤) = ((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))))
152 mpteq1 5121 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = (𝐹‘(𝑚𝑛)) → (𝑣𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
153152rneqd 5776 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = (𝐹‘(𝑚𝑛)) → ran (𝑣𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))
154153uneq2d 4093 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝐹‘(𝑚𝑛)) → ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
155149, 154iuneq12d 4912 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝐹‘(𝑚𝑛)) → 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣})) = 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})))
156151, 155uneq12d 4094 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝐹‘(𝑚𝑛)) → ((𝑤 𝑤) ∪ 𝑢𝑤 ({𝒫 𝑢, 𝑢} ∪ ran (𝑣𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
1574, 45, 156frsucmpt2w 8062 . . . . . . . . . . . . . . . 16 (((𝑚𝑛) ∈ ω ∧ (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
158107, 148, 157sylancl 589 . . . . . . . . . . . . . . 15 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹‘suc (𝑚𝑛)) = (((𝐹‘(𝑚𝑛)) ∪ (𝐹‘(𝑚𝑛))) ∪ 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣}))))
159140, 158sseqtrrid 3971 . . . . . . . . . . . . . 14 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚𝑛)))
160 fvssunirn 6678 . . . . . . . . . . . . . . 15 (𝐹‘suc (𝑚𝑛)) ⊆ ran 𝐹
161160, 1sseqtrri 3955 . . . . . . . . . . . . . 14 (𝐹‘suc (𝑚𝑛)) ⊆ 𝑈
162159, 161sstrdi 3930 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑢 ∈ (𝐹‘(𝑚𝑛))({𝒫 𝑢, 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈)
163139, 162sstrd 3928 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ({𝒫 𝑎, 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈)
164163unssbd 4118 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈)
165 ssun2 4103 . . . . . . . . . . . . . . . . . . 19 𝑛 ⊆ (𝑚𝑛)
166 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑚𝑛) → 𝑖 = (𝑚𝑛))
167165, 166sseqtrrid 3971 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑚𝑛) → 𝑛𝑖)
168167biantrud 535 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛𝑖)))
169168bicomd 226 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝑛 ∈ ω ∧ 𝑛𝑖) ↔ 𝑛 ∈ ω))
170 fveq2 6649 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑚𝑛) → (𝐹𝑖) = (𝐹‘(𝑚𝑛)))
171170sseq2d 3950 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑚𝑛) → ((𝐹𝑛) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
172169, 171imbi12d 348 . . . . . . . . . . . . . . 15 (𝑖 = (𝑚𝑛) → (((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)) ↔ (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))))
173 eleq1w 2875 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω))
174173anbi2d 631 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω)))
175 sseq1 3943 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝑚𝑖𝑛𝑖))
176174, 175anbi12d 633 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖)))
177 fveq2 6649 . . . . . . . . . . . . . . . . . . 19 (𝑚 = 𝑛 → (𝐹𝑚) = (𝐹𝑛))
178177sseq1d 3949 . . . . . . . . . . . . . . . . . 18 (𝑚 = 𝑛 → ((𝐹𝑚) ⊆ (𝐹𝑖) ↔ (𝐹𝑛) ⊆ (𝐹𝑖)))
179176, 178imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))))
180110, 112, 114, 112, 117, 129findsg 7594 . . . . . . . . . . . . . . . . 17 (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚𝑖) → (𝐹𝑚) ⊆ (𝐹𝑖))
181179, 180chvarvv 2005 . . . . . . . . . . . . . . . 16 (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖))
182181expl 461 . . . . . . . . . . . . . . 15 (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛𝑖) → (𝐹𝑛) ⊆ (𝐹𝑖)))
183172, 182vtoclga 3525 . . . . . . . . . . . . . 14 ((𝑚𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛))))
184107, 105, 183sylc 65 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → (𝐹𝑛) ⊆ (𝐹‘(𝑚𝑛)))
185 simprr 772 . . . . . . . . . . . . 13 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹𝑛))
186184, 185sseldd 3919 . . . . . . . . . . . 12 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → 𝑏 ∈ (𝐹‘(𝑚𝑛)))
187 prex 5301 . . . . . . . . . . . 12 {𝑎, 𝑏} ∈ V
188 eqid 2801 . . . . . . . . . . . . 13 (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣})
189 preq2 4633 . . . . . . . . . . . . 13 (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏})
190188, 189elrnmpt1s 5797 . . . . . . . . . . . 12 ((𝑏 ∈ (𝐹‘(𝑚𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
191186, 187, 190sylancl 589 . . . . . . . . . . 11 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚𝑛)) ↦ {𝑎, 𝑣}))
192164, 191sseldd 3919 . . . . . . . . . 10 (((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹𝑛))) → {𝑎, 𝑏} ∈ 𝑈)
193192rexlimdvaa 3247 . . . . . . . . 9 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹𝑛) → {𝑎, 𝑏} ∈ 𝑈))
194102, 193syl5bi 245 . . . . . . . 8 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → (𝑏𝑈 → {𝑎, 𝑏} ∈ 𝑈))
195194ralrimiv 3151 . . . . . . 7 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)
19697, 98, 1953jca 1125 . . . . . 6 ((𝐴𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹𝑚))) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
197196rexlimdvaa 3247 . . . . 5 (𝐴𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹𝑚) → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
1989, 197syl5bi 245 . . . 4 (𝐴𝑉 → (𝑎𝑈 → ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
199198ralrimiv 3151 . . 3 (𝐴𝑉 → ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))
200 rdgfun 8039 . . . . . . . . 9 Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o))
201 omex 9094 . . . . . . . . 9 ω ∈ V
202 resfunexg 6959 . . . . . . . . 9 ((Fun rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ∧ ω ∈ V) → (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) ∈ V)
203200, 201, 202mp2an 691 . . . . . . . 8 (rec((𝑧 ∈ V ↦ ((𝑧 𝑧) ∪ 𝑥𝑧 ({𝒫 𝑥, 𝑥} ∪ ran (𝑦𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) ∈ V
2044, 203eqeltri 2889 . . . . . . 7 𝐹 ∈ V
205204rnex 7603 . . . . . 6 ran 𝐹 ∈ V
206205uniex 7451 . . . . 5 ran 𝐹 ∈ V
2071, 206eqeltri 2889 . . . 4 𝑈 ∈ V
208 iswun 10119 . . . 4 (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈))))
209207, 208ax-mp 5 . . 3 (𝑈 ∈ WUni ↔ (Tr 𝑈𝑈 ≠ ∅ ∧ ∀𝑎𝑈 ( 𝑎𝑈 ∧ 𝒫 𝑎𝑈 ∧ ∀𝑏𝑈 {𝑎, 𝑏} ∈ 𝑈)))
21064, 78, 199, 209syl3anbrc 1340 . 2 (𝐴𝑉𝑈 ∈ WUni)
21174unssad 4117 . 2 (𝐴𝑉𝐴𝑈)
212210, 211jca 515 1 (𝐴𝑉 → (𝑈 ∈ WUni ∧ 𝐴𝑈))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2112  wne 2990  wral 3109  wrex 3110  Vcvv 3444  cun 3882  wss 3884  c0 4246  𝒫 cpw 4500  {cpr 4530   cuni 4803   ciun 4884  cmpt 5113  Tr wtr 5139  ran crn 5524  cres 5525  Ord word 6162  Oncon0 6163  suc csuc 6165  Fun wfun 6322   Fn wfn 6323  cfv 6328  ωcom 7564  reccrdg 8032  1oc1o 8082  WUnicwun 10115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-om 7565  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-wun 10117
This theorem is referenced by:  wunex  10154  wuncval2  10162
  Copyright terms: Public domain W3C validator