Metamath Proof Explorer

Theorem dfrdg4

Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfrdg4 ⊒rec⁑FA=⋃π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβˆ–dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό

Proof

Step Hyp Ref Expression
1 dfrdg3 ⊒rec⁑FA=⋃f|βˆƒx∈OnfFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
2 an12 ⊒x∈On∧fFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔fFnx∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
3 df-fn ⊒fFnx↔Fun⁑f∧dom⁑f=x
4 ancom ⊒Fun⁑f∧dom⁑f=x↔dom⁑f=x∧Fun⁑f
5 eqcom ⊒dom⁑f=x↔x=dom⁑f
6 5 anbi1i ⊒dom⁑f=x∧Fun⁑f↔x=dom⁑f∧Fun⁑f
7 3 4 6 3bitri ⊒fFnx↔x=dom⁑f∧Fun⁑f
8 7 anbi1i ⊒fFnx∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔x=dom⁑f∧Fun⁑f∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
9 anass ⊒x=dom⁑f∧Fun⁑f∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔x=dom⁑f∧Fun⁑f∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
10 2 8 9 3bitri ⊒x∈On∧fFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔x=dom⁑f∧Fun⁑f∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
11 10 exbii βŠ’βˆƒxx∈On∧fFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†”βˆƒxx=dom⁑f∧Fun⁑f∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
12 vex ⊒f∈V
13 12 dmex ⊒dom⁑f∈V
14 eleq1 ⊒x=dom⁑fβ†’x∈On↔dom⁑f∈On
15 raleq ⊒x=dom⁑fβ†’βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†”βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
16 14 15 anbi12d ⊒x=dom⁑fβ†’x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
17 16 anbi2d ⊒x=dom⁑fβ†’Fun⁑f∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
18 13 17 ceqsexv βŠ’βˆƒxx=dom⁑f∧Fun⁑f∧x∈Onβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
19 11 18 bitri βŠ’βˆƒxx∈On∧fFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
20 df-rex βŠ’βˆƒx∈OnfFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†”βˆƒxx∈On∧fFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
21 eldif ⊒f∈π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβˆ–dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”f∈π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1On∧¬f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό
22 elin ⊒f∈π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1On↔f∈π–₯π—Žπ—‡π—Œβˆ§fβˆˆπ–£π—ˆπ—†π–Ίπ—‚π—‡-1On
23 12 elfuns ⊒f∈π–₯π—Žπ—‡π—Œβ†”Fun⁑f
24 12 elima ⊒fβˆˆπ–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβ†”βˆƒx∈Onxπ–£π—ˆπ—†π–Ίπ—‚π—‡-1f
25 df-rex βŠ’βˆƒx∈Onxπ–£π—ˆπ—†π–Ίπ—‚π—‡-1fβ†”βˆƒxx∈On∧xπ–£π—ˆπ—†π–Ίπ—‚π—‡-1f
26 vex ⊒x∈V
27 26 12 brcnv ⊒xπ–£π—ˆπ—†π–Ίπ—‚π—‡-1f↔fπ–£π—ˆπ—†π–Ίπ—‚π—‡x
28 12 26 brdomain ⊒fπ–£π—ˆπ—†π–Ίπ—‚π—‡x↔x=dom⁑f
29 27 28 bitri ⊒xπ–£π—ˆπ—†π–Ίπ—‚π—‡-1f↔x=dom⁑f
30 29 anbi1ci ⊒x∈On∧xπ–£π—ˆπ—†π–Ίπ—‚π—‡-1f↔x=dom⁑f∧x∈On
31 30 exbii βŠ’βˆƒxx∈On∧xπ–£π—ˆπ—†π–Ίπ—‚π—‡-1fβ†”βˆƒxx=dom⁑f∧x∈On
32 13 14 ceqsexv βŠ’βˆƒxx=dom⁑f∧x∈On↔dom⁑f∈On
33 31 32 bitri βŠ’βˆƒxx∈On∧xπ–£π—ˆπ—†π–Ίπ—‚π—‡-1f↔dom⁑f∈On
34 24 25 33 3bitri ⊒fβˆˆπ–£π—ˆπ—†π–Ίπ—‚π—‡-1On↔dom⁑f∈On
35 23 34 anbi12i ⊒f∈π–₯π—Žπ—‡π—Œβˆ§fβˆˆπ–£π—ˆπ—†π–Ίπ—‚π—‡-1On↔Fun⁑f∧dom⁑f∈On
36 22 35 bitri ⊒f∈π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1On↔Fun⁑f∧dom⁑f∈On
37 36 anbi1i ⊒f∈π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1On∧¬f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”Fun⁑f∧dom⁑f∈On∧¬f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό
38 brdif ⊒fE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔fE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡y∧¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy
39 vex ⊒y∈V
40 12 39 brco ⊒fE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡yβ†”βˆƒxfπ–£π—ˆπ—†π–Ίπ—‚π—‡x∧xE-1y
41 28 anbi1i ⊒fπ–£π—ˆπ—†π–Ίπ—‚π—‡x∧xE-1y↔x=dom⁑f∧xE-1y
42 41 exbii βŠ’βˆƒxfπ–£π—ˆπ—†π–Ίπ—‚π—‡x∧xE-1yβ†”βˆƒxx=dom⁑f∧xE-1y
43 breq1 ⊒x=dom⁑fβ†’xE-1y↔dom⁑fE-1y
44 13 43 ceqsexv βŠ’βˆƒxx=dom⁑f∧xE-1y↔dom⁑fE-1y
45 42 44 bitri βŠ’βˆƒxfπ–£π—ˆπ—†π–Ίπ—‚π—‡x∧xE-1y↔dom⁑fE-1y
46 13 39 brcnv ⊒dom⁑fE-1y↔yEdom⁑f
47 13 epeli ⊒yEdom⁑f↔y∈dom⁑f
48 46 47 bitri ⊒dom⁑fE-1y↔y∈dom⁑f
49 40 45 48 3bitri ⊒fE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡y↔y∈dom⁑f
50 49 anbi1i ⊒fE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡y∧¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔y∈dom⁑f∧¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy
51 38 50 bitri ⊒fE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔y∈dom⁑f∧¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy
52 onelon ⊒dom⁑f∈On∧y∈dom⁑fβ†’y∈On
53 52 3adant1 ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’y∈On
54 brun ⊒fyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔fyVΓ—βˆ…Γ—β‹ƒAx∨fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx
55 brxp ⊒fyVΓ—βˆ…Γ—β‹ƒAx↔fy∈VΓ—βˆ…βˆ§xβˆˆβ‹ƒA
56 opelxp ⊒fy∈VΓ—βˆ…β†”f∈V∧yβˆˆβˆ…
57 12 56 mpbiran ⊒fy∈VΓ—βˆ…β†”yβˆˆβˆ…
58 velsn ⊒yβˆˆβˆ…β†”y=βˆ…
59 57 58 bitri ⊒fy∈VΓ—βˆ…β†”y=βˆ…
60 velsn ⊒xβˆˆβ‹ƒA↔x=⋃A
61 59 60 anbi12i ⊒fy∈VΓ—βˆ…βˆ§xβˆˆβ‹ƒA↔y=βˆ…βˆ§x=⋃A
62 55 61 bitri ⊒fyVΓ—βˆ…Γ—β‹ƒAx↔y=βˆ…βˆ§x=⋃A
63 brun ⊒fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œx∨fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx
64 26 brresi ⊒fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œx↔fy∈VΓ—π–«π—‚π—†π—‚π—π—Œβˆ§fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€x
65 opelxp ⊒fy∈VΓ—π–«π—‚π—†π—‚π—π—Œβ†”f∈V∧yβˆˆπ–«π—‚π—†π—‚π—π—Œ
66 12 65 mpbiran ⊒fy∈VΓ—π–«π—‚π—†π—‚π—π—Œβ†”yβˆˆπ–«π—‚π—†π—‚π—π—Œ
67 39 ellimits ⊒yβˆˆπ–«π—‚π—†π—‚π—π—Œβ†”Lim⁑y
68 66 67 bitri ⊒fy∈VΓ—π–«π—‚π—†π—‚π—π—Œβ†”Lim⁑y
69 opex ⊒fy∈V
70 69 26 brco ⊒fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€xβ†”βˆƒzfy𝖨𝗆𝗀z∧zπ–‘π—‚π—€π–Όπ—Žπ—‰x
71 vex ⊒z∈V
72 12 39 71 brimg ⊒fy𝖨𝗆𝗀z↔z=fy
73 26 brbigcup ⊒zπ–‘π—‚π—€π–Όπ—Žπ—‰x↔⋃z=x
74 72 73 anbi12i ⊒fy𝖨𝗆𝗀z∧zπ–‘π—‚π—€π–Όπ—Žπ—‰x↔z=fyβˆ§β‹ƒz=x
75 74 exbii βŠ’βˆƒzfy𝖨𝗆𝗀z∧zπ–‘π—‚π—€π–Όπ—Žπ—‰xβ†”βˆƒzz=fyβˆ§β‹ƒz=x
76 12 imaex ⊒fy∈V
77 unieq ⊒z=fy→⋃z=⋃fy
78 77 eqeq1d ⊒z=fy→⋃z=x↔⋃fy=x
79 76 78 ceqsexv βŠ’βˆƒzz=fyβˆ§β‹ƒz=x↔⋃fy=x
80 eqcom βŠ’β‹ƒfy=x↔x=⋃fy
81 79 80 bitri βŠ’βˆƒzz=fyβˆ§β‹ƒz=x↔x=⋃fy
82 70 75 81 3bitri ⊒fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€x↔x=⋃fy
83 68 82 anbi12i ⊒fy∈VΓ—π–«π—‚π—†π—‚π—π—Œβˆ§fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€x↔Lim⁑y∧x=⋃fy
84 64 83 bitri ⊒fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œx↔Lim⁑y∧x=⋃fy
85 26 brresi ⊒fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔fy∈VΓ—ranβ‘π–²π—Žπ–Όπ–Όβˆ§fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰x
86 opelxp ⊒fy∈VΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”f∈V∧y∈ranβ‘π–²π—Žπ–Όπ–Ό
87 12 86 mpbiran ⊒fy∈VΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”y∈ranβ‘π–²π—Žπ–Όπ–Ό
88 39 elrn ⊒y∈ranβ‘π–²π—Žπ–Όπ–Όβ†”βˆƒzzπ–²π—Žπ–Όπ–Όy
89 71 39 brsuccf ⊒zπ–²π—Žπ–Όπ–Όy↔y=suc⁑z
90 89 exbii βŠ’βˆƒzzπ–²π—Žπ–Όπ–Όyβ†”βˆƒzy=suc⁑z
91 87 88 90 3bitri ⊒fy∈VΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”βˆƒzy=suc⁑z
92 69 26 brco ⊒fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰xβ†”βˆƒafyπ– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰a∧aπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fx
93 vex ⊒a∈V
94 69 93 brco ⊒fyπ– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰aβ†”βˆƒzfypprodIπ–‘π—‚π—€π–Όπ—Žπ—‰z∧z𝖠𝗉𝗉𝗅𝗒a
95 12 39 71 brpprod3a ⊒fypprodIπ–‘π—‚π—€π–Όπ—Žπ—‰zβ†”βˆƒaβˆƒbz=ab∧fIa∧yπ–‘π—‚π—€π–Όπ—Žπ—‰b
96 3anrot ⊒z=ab∧fIa∧yπ–‘π—‚π—€π–Όπ—Žπ—‰b↔fIa∧yπ–‘π—‚π—€π–Όπ—Žπ—‰b∧z=ab
97 93 ideq ⊒fIa↔f=a
98 equcom ⊒f=a↔a=f
99 97 98 bitri ⊒fIa↔a=f
100 vex ⊒b∈V
101 100 brbigcup ⊒yπ–‘π—‚π—€π–Όπ—Žπ—‰b↔⋃y=b
102 eqcom βŠ’β‹ƒy=b↔b=⋃y
103 101 102 bitri ⊒yπ–‘π—‚π—€π–Όπ—Žπ—‰b↔b=⋃y
104 biid ⊒z=ab↔z=ab
105 99 103 104 3anbi123i ⊒fIa∧yπ–‘π—‚π—€π–Όπ—Žπ—‰b∧z=ab↔a=f∧b=⋃y∧z=ab
106 96 105 bitri ⊒z=ab∧fIa∧yπ–‘π—‚π—€π–Όπ—Žπ—‰b↔a=f∧b=⋃y∧z=ab
107 106 2exbii βŠ’βˆƒaβˆƒbz=ab∧fIa∧yπ–‘π—‚π—€π–Όπ—Žπ—‰bβ†”βˆƒaβˆƒba=f∧b=⋃y∧z=ab
108 vuniex βŠ’β‹ƒy∈V
109 opeq1 ⊒a=fβ†’ab=fb
110 109 eqeq2d ⊒a=fβ†’z=ab↔z=fb
111 opeq2 ⊒b=⋃yβ†’fb=f⋃y
112 111 eqeq2d ⊒b=⋃yβ†’z=fb↔z=f⋃y
113 12 108 110 112 ceqsex2v βŠ’βˆƒaβˆƒba=f∧b=⋃y∧z=ab↔z=f⋃y
114 95 107 113 3bitri ⊒fypprodIπ–‘π—‚π—€π–Όπ—Žπ—‰z↔z=f⋃y
115 114 anbi1i ⊒fypprodIπ–‘π—‚π—€π–Όπ—Žπ—‰z∧z𝖠𝗉𝗉𝗅𝗒a↔z=f⋃y∧z𝖠𝗉𝗉𝗅𝗒a
116 115 exbii βŠ’βˆƒzfypprodIπ–‘π—‚π—€π–Όπ—Žπ—‰z∧z𝖠𝗉𝗉𝗅𝗒aβ†”βˆƒzz=f⋃y∧z𝖠𝗉𝗉𝗅𝗒a
117 opex ⊒f⋃y∈V
118 breq1 ⊒z=f⋃yβ†’z𝖠𝗉𝗉𝗅𝗒a↔f⋃y𝖠𝗉𝗉𝗅𝗒a
119 117 118 ceqsexv βŠ’βˆƒzz=f⋃y∧z𝖠𝗉𝗉𝗅𝗒a↔f⋃y𝖠𝗉𝗉𝗅𝗒a
120 12 108 93 brapply ⊒f⋃y𝖠𝗉𝗉𝗅𝗒a↔a=f⁑⋃y
121 119 120 bitri βŠ’βˆƒzz=f⋃y∧z𝖠𝗉𝗉𝗅𝗒a↔a=f⁑⋃y
122 94 116 121 3bitri ⊒fyπ– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰a↔a=f⁑⋃y
123 93 26 brfullfun ⊒aπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fx↔x=F⁑a
124 122 123 anbi12i ⊒fyπ– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰a∧aπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fx↔a=f⁑⋃y∧x=F⁑a
125 124 exbii βŠ’βˆƒafyπ– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰a∧aπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fxβ†”βˆƒaa=f⁑⋃y∧x=F⁑a
126 fvex ⊒f⁑⋃y∈V
127 fveq2 ⊒a=f⁑⋃yβ†’F⁑a=F⁑f⁑⋃y
128 127 eqeq2d ⊒a=f⁑⋃yβ†’x=F⁑a↔x=F⁑f⁑⋃y
129 126 128 ceqsexv βŠ’βˆƒaa=f⁑⋃y∧x=F⁑a↔x=F⁑f⁑⋃y
130 92 125 129 3bitri ⊒fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰x↔x=F⁑f⁑⋃y
131 91 130 anbi12i ⊒fy∈VΓ—ranβ‘π–²π—Žπ–Όπ–Όβˆ§fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰xβ†”βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
132 85 131 bitri ⊒fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όxβ†”βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
133 84 132 orbi12i ⊒fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œx∨fyπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
134 63 133 bitri ⊒fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
135 62 134 orbi12i ⊒fyVΓ—βˆ…Γ—β‹ƒAx∨fyπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
136 54 135 bitri ⊒fyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
137 onzsl ⊒y∈On↔y=βˆ…βˆ¨βˆƒz∈Ony=suc⁑z∨y∈V∧Lim⁑y
138 nlim0 ⊒¬Limβ‘βˆ…
139 limeq ⊒y=βˆ…β†’Lim⁑y↔Limβ‘βˆ…
140 138 139 mtbiri ⊒y=βˆ…β†’Β¬Lim⁑y
141 140 intnanrd ⊒y=βˆ…β†’Β¬Lim⁑y∧x=⋃fy
142 nsuceq0 ⊒suc⁑zβ‰ βˆ…
143 neeq2 ⊒y=βˆ…β†’suc⁑zβ‰ y↔suc⁑zβ‰ βˆ…
144 142 143 mpbiri ⊒y=βˆ…β†’suc⁑zβ‰ y
145 144 necomd ⊒y=βˆ…β†’yβ‰ suc⁑z
146 145 neneqd ⊒y=βˆ…β†’Β¬y=suc⁑z
147 146 nexdv ⊒y=βˆ…β†’Β¬βˆƒzy=suc⁑z
148 147 intnanrd ⊒y=βˆ…β†’Β¬βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
149 ioran ⊒¬Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y↔¬Lim⁑y∧x=⋃fyβˆ§Β¬βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
150 141 148 149 sylanbrc ⊒y=βˆ…β†’Β¬Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
151 orel2 ⊒¬Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A
152 150 151 syl ⊒y=βˆ…β†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A
153 iftrue ⊒y=βˆ…β†’ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y=ifA∈VAβˆ…
154 unisnif βŠ’β‹ƒA=ifA∈VAβˆ…
155 153 154 eqtr4di ⊒y=βˆ…β†’ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y=⋃A
156 155 eqeq2d ⊒y=βˆ…β†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔x=⋃A
157 156 biimprd ⊒y=βˆ…β†’x=⋃Aβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
158 157 adantld ⊒y=βˆ…β†’y=βˆ…βˆ§x=⋃Aβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
159 152 158 syld ⊒y=βˆ…β†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
160 156 biimpd ⊒y=βˆ…β†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’x=⋃A
161 160 anc2li ⊒y=βˆ…β†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A
162 orc ⊒y=βˆ…βˆ§x=⋃Aβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
163 161 162 syl6 ⊒y=βˆ…β†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
164 159 163 impbid ⊒y=βˆ…β†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
165 neeq1 ⊒y=suc⁑zβ†’yβ‰ βˆ…β†”suc⁑zβ‰ βˆ…
166 142 165 mpbiri ⊒y=suc⁑zβ†’yβ‰ βˆ…
167 166 neneqd ⊒y=suc⁑zβ†’Β¬y=βˆ…
168 167 intnanrd ⊒y=suc⁑zβ†’Β¬y=βˆ…βˆ§x=⋃A
169 168 rexlimivw βŠ’βˆƒz∈Ony=suc⁑zβ†’Β¬y=βˆ…βˆ§x=⋃A
170 orel1 ⊒¬y=βˆ…βˆ§x=⋃Aβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
171 169 170 syl βŠ’βˆƒz∈Ony=suc⁑zβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
172 nlimsucg ⊒z∈Vβ†’Β¬Lim⁑suc⁑z
173 172 elv ⊒¬Lim⁑suc⁑z
174 limeq ⊒y=suc⁑zβ†’Lim⁑y↔Lim⁑suc⁑z
175 173 174 mtbiri ⊒y=suc⁑zβ†’Β¬Lim⁑y
176 175 rexlimivw βŠ’βˆƒz∈Ony=suc⁑zβ†’Β¬Lim⁑y
177 176 intnanrd βŠ’βˆƒz∈Ony=suc⁑zβ†’Β¬Lim⁑y∧x=⋃fy
178 orel1 ⊒¬Lim⁑y∧x=⋃fyβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
179 177 178 syl βŠ’βˆƒz∈Ony=suc⁑zβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
180 142 neii ⊒¬suc⁑z=βˆ…
181 180 iffalsei ⊒ifsuc⁑z=βˆ…ifA∈VAβˆ…ifLim⁑suc⁑z⋃fyF⁑f⁑⋃suc⁑z=ifLim⁑suc⁑z⋃fyF⁑f⁑⋃suc⁑z
182 iffalse ⊒¬Lim⁑suc⁑zβ†’ifLim⁑suc⁑z⋃fyF⁑f⁑⋃suc⁑z=F⁑f⁑⋃suc⁑z
183 71 172 182 mp2b ⊒ifLim⁑suc⁑z⋃fyF⁑f⁑⋃suc⁑z=F⁑f⁑⋃suc⁑z
184 181 183 eqtri ⊒ifsuc⁑z=βˆ…ifA∈VAβˆ…ifLim⁑suc⁑z⋃fyF⁑f⁑⋃suc⁑z=F⁑f⁑⋃suc⁑z
185 eqeq1 ⊒y=suc⁑zβ†’y=βˆ…β†”suc⁑z=βˆ…
186 unieq ⊒y=suc⁑z→⋃y=⋃suc⁑z
187 186 fveq2d ⊒y=suc⁑zβ†’f⁑⋃y=f⁑⋃suc⁑z
188 187 fveq2d ⊒y=suc⁑zβ†’F⁑f⁑⋃y=F⁑f⁑⋃suc⁑z
189 174 188 ifbieq2d ⊒y=suc⁑zβ†’ifLim⁑y⋃fyF⁑f⁑⋃y=ifLim⁑suc⁑z⋃fyF⁑f⁑⋃suc⁑z
190 185 189 ifbieq2d ⊒y=suc⁑zβ†’ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y=ifsuc⁑z=βˆ…ifA∈VAβˆ…ifLim⁑suc⁑z⋃fyF⁑f⁑⋃suc⁑z
191 184 190 188 3eqtr4a ⊒y=suc⁑zβ†’ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y=F⁑f⁑⋃y
192 191 rexlimivw βŠ’βˆƒz∈Ony=suc⁑zβ†’ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y=F⁑f⁑⋃y
193 192 eqeq2d βŠ’βˆƒz∈Ony=suc⁑zβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔x=F⁑f⁑⋃y
194 193 biimprd βŠ’βˆƒz∈Ony=suc⁑zβ†’x=F⁑f⁑⋃yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
195 194 adantld βŠ’βˆƒz∈Ony=suc⁑zβ†’βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
196 171 179 195 3syld βŠ’βˆƒz∈Ony=suc⁑zβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
197 rexex βŠ’βˆƒz∈Ony=suc⁑zβ†’βˆƒzy=suc⁑z
198 193 biimpd βŠ’βˆƒz∈Ony=suc⁑zβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’x=F⁑f⁑⋃y
199 olc βŠ’βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
200 199 olcd βŠ’βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
201 197 198 200 syl6an βŠ’βˆƒz∈Ony=suc⁑zβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
202 196 201 impbid βŠ’βˆƒz∈Ony=suc⁑zβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
203 140 con2i ⊒Lim⁑yβ†’Β¬y=βˆ…
204 203 intnanrd ⊒Lim⁑yβ†’Β¬y=βˆ…βˆ§x=⋃A
205 204 170 syl ⊒Lim⁑yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
206 175 exlimiv βŠ’βˆƒzy=suc⁑zβ†’Β¬Lim⁑y
207 206 con2i ⊒Lim⁑yβ†’Β¬βˆƒzy=suc⁑z
208 207 intnanrd ⊒Lim⁑yβ†’Β¬βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
209 orel2 βŠ’Β¬βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fy
210 208 209 syl ⊒Lim⁑yβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fy
211 203 iffalsed ⊒Lim⁑yβ†’ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y=ifLim⁑y⋃fyF⁑f⁑⋃y
212 iftrue ⊒Lim⁑yβ†’ifLim⁑y⋃fyF⁑f⁑⋃y=⋃fy
213 211 212 eqtrd ⊒Lim⁑yβ†’ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y=⋃fy
214 213 eqeq2d ⊒Lim⁑yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔x=⋃fy
215 214 biimprd ⊒Lim⁑yβ†’x=⋃fyβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
216 215 adantld ⊒Lim⁑yβ†’Lim⁑y∧x=⋃fyβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
217 205 210 216 3syld ⊒Lim⁑yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
218 217 adantl ⊒y∈V∧Lim⁑yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
219 214 biimpd ⊒Lim⁑yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’x=⋃fy
220 219 anc2li ⊒Lim⁑yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’Lim⁑y∧x=⋃fy
221 orc ⊒Lim⁑y∧x=⋃fyβ†’Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
222 221 olcd ⊒Lim⁑y∧x=⋃fyβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
223 220 222 syl6 ⊒Lim⁑yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
224 223 adantl ⊒y∈V∧Lim⁑yβ†’x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y
225 218 224 impbid ⊒y∈V∧Lim⁑yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
226 164 202 225 3jaoi ⊒y=βˆ…βˆ¨βˆƒz∈Ony=suc⁑z∨y∈V∧Lim⁑yβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
227 137 226 sylbi ⊒y∈Onβ†’y=βˆ…βˆ§x=⋃A∨Lim⁑y∧x=⋃fyβˆ¨βˆƒzy=suc⁑z∧x=F⁑f⁑⋃y↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
228 136 227 bitrid ⊒y∈Onβ†’fyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
229 53 228 syl ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’fyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
230 26 69 brcnv ⊒x𝖠𝗉𝗉𝗅𝗒-1fy↔fy𝖠𝗉𝗉𝗅𝗒x
231 12 39 26 brapply ⊒fy𝖠𝗉𝗉𝗅𝗒x↔x=f⁑y
232 230 231 bitri ⊒x𝖠𝗉𝗉𝗅𝗒-1fy↔x=f⁑y
233 232 a1i ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’x𝖠𝗉𝗉𝗅𝗒-1fy↔x=f⁑y
234 229 233 anbi12d ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’fyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx∧x𝖠𝗉𝗉𝗅𝗒-1fy↔x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y∧x=f⁑y
235 234 biancomd ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’fyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx∧x𝖠𝗉𝗉𝗅𝗒-1fy↔x=f⁑y∧x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
236 235 exbidv ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’βˆƒxfyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx∧x𝖠𝗉𝗉𝗅𝗒-1fyβ†”βˆƒxx=f⁑y∧x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
237 df-br ⊒fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔fy∈π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό
238 69 elfix ⊒fy∈π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”fy𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όfy
239 69 69 brco ⊒fy𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όfyβ†”βˆƒxfyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx∧x𝖠𝗉𝗉𝗅𝗒-1fy
240 237 238 239 3bitri ⊒fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όyβ†”βˆƒxfyVΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όx∧x𝖠𝗉𝗉𝗅𝗒-1fy
241 fvex ⊒f⁑y∈V
242 241 eqvinc ⊒f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†”βˆƒxx=f⁑y∧x=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
243 236 240 242 3bitr4g ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
244 243 notbid ⊒Fun⁑f∧dom⁑f∈On∧y∈dom⁑fβ†’Β¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔¬f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
245 244 3expia ⊒Fun⁑f∧dom⁑f∈Onβ†’y∈dom⁑fβ†’Β¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔¬f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
246 245 pm5.32d ⊒Fun⁑f∧dom⁑f∈Onβ†’y∈dom⁑f∧¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔y∈dom⁑f∧¬f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
247 annim ⊒y∈dom⁑f∧¬f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔¬y∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
248 246 247 bitrdi ⊒Fun⁑f∧dom⁑f∈Onβ†’y∈dom⁑f∧¬fπ–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔¬y∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
249 51 248 bitrid ⊒Fun⁑f∧dom⁑f∈Onβ†’fE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy↔¬y∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
250 249 exbidv ⊒Fun⁑f∧dom⁑f∈Onβ†’βˆƒyfE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όyβ†”βˆƒyΒ¬y∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
251 exnal βŠ’βˆƒyΒ¬y∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†”Β¬βˆ€yy∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
252 250 251 bitr2di ⊒Fun⁑f∧dom⁑f∈Onβ†’Β¬βˆ€yy∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†”βˆƒyfE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy
253 12 eldm ⊒f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”βˆƒyfE-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όy
254 252 253 bitr4di ⊒Fun⁑f∧dom⁑f∈Onβ†’Β¬βˆ€yy∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό
255 254 con1bid ⊒Fun⁑f∧dom⁑f∈Onβ†’Β¬f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”βˆ€yy∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
256 df-ral βŠ’βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃yβ†”βˆ€yy∈dom⁑fβ†’f⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
257 255 256 bitr4di ⊒Fun⁑f∧dom⁑f∈Onβ†’Β¬f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
258 257 pm5.32i ⊒Fun⁑f∧dom⁑f∈On∧¬f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
259 anass ⊒Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y↔Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
260 258 259 bitri ⊒Fun⁑f∧dom⁑f∈On∧¬f∈dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
261 21 37 260 3bitri ⊒f∈π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβˆ–dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”Fun⁑f∧dom⁑f∈Onβˆ§βˆ€y∈dom⁑ff⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
262 19 20 261 3bitr4ri ⊒f∈π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβˆ–dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Όβ†”βˆƒx∈OnfFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
263 262 eqabi ⊒π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβˆ–dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό=f|βˆƒx∈OnfFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
264 263 unieqi βŠ’β‹ƒπ–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβˆ–dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό=⋃f|βˆƒx∈OnfFnxβˆ§βˆ€y∈xf⁑y=ify=βˆ…ifA∈VAβˆ…ifLim⁑y⋃fyF⁑f⁑⋃y
265 1 264 eqtr4i ⊒rec⁑FA=⋃π–₯π—Žπ—‡π—Œβˆ©π–£π—ˆπ—†π–Ίπ—‚π—‡-1Onβˆ–dom⁑E-1βˆ˜π–£π—ˆπ—†π–Ίπ—‚π—‡βˆ–π–₯𝗂𝗑𝖠𝗉𝗉𝗅𝗒-1∘VΓ—βˆ…Γ—β‹ƒAβˆͺπ–‘π—‚π—€π–Όπ—Žπ—‰βˆ˜π–¨π—†π—€β†ΎVΓ—π–«π—‚π—†π—‚π—π—Œβˆͺπ–₯π—Žπ—…π—…π–₯π—Žπ—‡Fβˆ˜π– π—‰π—‰π—…π—’βˆ˜pprodIπ–‘π—‚π—€π–Όπ—Žπ—‰β†ΎVΓ—ranβ‘π–²π—Žπ–Όπ–Ό