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 ⁡ F A = ⋃ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∖ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼

Proof

Step Hyp Ref Expression
1 dfrdg3 ⊢ rec ⁡ F A = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
2 an12 ⊢ x ∈ On ∧ f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ f Fn x ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
3 df-fn ⊢ f Fn x ↔ 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 ⊢ f Fn x ↔ x = dom ⁡ f ∧ Fun ⁡ f
8 7 anbi1i ⊢ f Fn x ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ x = dom ⁡ f ∧ Fun ⁡ f ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
9 anass ⊢ x = dom ⁡ f ∧ Fun ⁡ f ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ x = dom ⁡ f ∧ Fun ⁡ f ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
10 2 8 9 3bitri ⊢ x ∈ On ∧ f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ x = dom ⁡ f ∧ Fun ⁡ f ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
11 10 exbii ⊢ ∃ x x ∈ On ∧ f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∃ x x = dom ⁡ f ∧ Fun ⁡ f ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ 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 ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
16 14 15 anbi12d ⊢ x = dom ⁡ f → x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
17 16 anbi2d ⊢ x = dom ⁡ f → Fun ⁡ f ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
18 13 17 ceqsexv ⊢ ∃ x x = dom ⁡ f ∧ Fun ⁡ f ∧ x ∈ On ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
19 11 18 bitri ⊢ ∃ x x ∈ On ∧ f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
20 df-rex ⊢ ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∃ x x ∈ On ∧ f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
21 eldif ⊢ f ∈ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∖ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ f ∈ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∧ ¬ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼
22 elin ⊢ f ∈ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ↔ f ∈ 𝖥𝗎𝗇𝗌 ∧ f ∈ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On
23 12 elfuns ⊢ f ∈ 𝖥𝗎𝗇𝗌 ↔ Fun ⁡ f
24 12 elima ⊢ f ∈ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ↔ ∃ x ∈ On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f
25 df-rex ⊢ ∃ x ∈ On x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f ↔ ∃ x x ∈ On ∧ x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f
26 vex ⊢ x ∈ V
27 26 12 brcnv ⊢ x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f ↔ f 𝖣𝗈𝗆𝖺𝗂𝗇 x
28 12 26 brdomain ⊢ f 𝖣𝗈𝗆𝖺𝗂𝗇 x ↔ x = dom ⁡ f
29 27 28 bitri ⊢ x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f ↔ x = dom ⁡ f
30 29 anbi1ci ⊢ x ∈ On ∧ x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f ↔ x = dom ⁡ f ∧ x ∈ On
31 30 exbii ⊢ ∃ x x ∈ On ∧ x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f ↔ ∃ x x = dom ⁡ f ∧ x ∈ On
32 13 14 ceqsexv ⊢ ∃ x x = dom ⁡ f ∧ x ∈ On ↔ dom ⁡ f ∈ On
33 31 32 bitri ⊢ ∃ x x ∈ On ∧ x 𝖣𝗈𝗆𝖺𝗂𝗇 -1 f ↔ dom ⁡ f ∈ On
34 24 25 33 3bitri ⊢ f ∈ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ↔ dom ⁡ f ∈ On
35 23 34 anbi12i ⊢ f ∈ 𝖥𝗎𝗇𝗌 ∧ f ∈ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On
36 22 35 bitri ⊢ f ∈ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On
37 36 anbi1i ⊢ f ∈ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∧ ¬ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ¬ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼
38 brdif ⊢ f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 y ∧ ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y
39 vex ⊢ y ∈ V
40 12 39 brco ⊢ f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 y ↔ ∃ x f 𝖣𝗈𝗆𝖺𝗂𝗇 x ∧ x E -1 y
41 28 anbi1i ⊢ f 𝖣𝗈𝗆𝖺𝗂𝗇 x ∧ x E -1 y ↔ x = dom ⁡ f ∧ x E -1 y
42 41 exbii ⊢ ∃ x f 𝖣𝗈𝗆𝖺𝗂𝗇 x ∧ x E -1 y ↔ ∃ x x = dom ⁡ f ∧ x E -1 y
43 breq1 ⊢ x = dom ⁡ f → x E -1 y ↔ dom ⁡ f E -1 y
44 13 43 ceqsexv ⊢ ∃ x x = dom ⁡ f ∧ x E -1 y ↔ dom ⁡ f E -1 y
45 42 44 bitri ⊢ ∃ x f 𝖣𝗈𝗆𝖺𝗂𝗇 x ∧ x E -1 y ↔ dom ⁡ f E -1 y
46 13 39 brcnv ⊢ dom ⁡ f E -1 y ↔ y E dom ⁡ f
47 13 epeli ⊢ y E dom ⁡ f ↔ y ∈ dom ⁡ f
48 46 47 bitri ⊢ dom ⁡ f E -1 y ↔ y ∈ dom ⁡ f
49 40 45 48 3bitri ⊢ f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 y ↔ y ∈ dom ⁡ f
50 49 anbi1i ⊢ f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 y ∧ ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ y ∈ dom ⁡ f ∧ ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y
51 38 50 bitri ⊢ f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ y ∈ dom ⁡ f ∧ ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ 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 ⊢ f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ f y V × ∅ × ⋃ A x ∨ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x
55 brxp ⊢ f y V × ∅ × ⋃ A x ↔ f y ∈ V × ∅ ∧ x ∈ ⋃ A
56 opelxp ⊢ f y ∈ V × ∅ ↔ f ∈ V ∧ y ∈ ∅
57 12 56 mpbiran ⊢ f y ∈ V × ∅ ↔ y ∈ ∅
58 velsn ⊢ y ∈ ∅ ↔ y = ∅
59 57 58 bitri ⊢ f y ∈ V × ∅ ↔ y = ∅
60 velsn ⊢ x ∈ ⋃ A ↔ x = ⋃ A
61 59 60 anbi12i ⊢ f y ∈ V × ∅ ∧ x ∈ ⋃ A ↔ y = ∅ ∧ x = ⋃ A
62 55 61 bitri ⊢ f y V × ∅ × ⋃ A x ↔ y = ∅ ∧ x = ⋃ A
63 brun ⊢ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 x ∨ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x
64 26 brresi ⊢ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 x ↔ f y ∈ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∧ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 x
65 opelxp ⊢ f y ∈ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ↔ f ∈ V ∧ y ∈ 𝖫𝗂𝗆𝗂𝗍𝗌
66 12 65 mpbiran ⊢ f y ∈ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ↔ y ∈ 𝖫𝗂𝗆𝗂𝗍𝗌
67 39 ellimits ⊢ y ∈ 𝖫𝗂𝗆𝗂𝗍𝗌 ↔ Lim ⁡ y
68 66 67 bitri ⊢ f y ∈ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ↔ Lim ⁡ y
69 opex ⊢ f y ∈ V
70 69 26 brco ⊢ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 x ↔ ∃ z f y 𝖨𝗆𝗀 z ∧ z 𝖡𝗂𝗀𝖼𝗎𝗉 x
71 vex ⊢ z ∈ V
72 12 39 71 brimg ⊢ f y 𝖨𝗆𝗀 z ↔ z = f y
73 26 brbigcup ⊢ z 𝖡𝗂𝗀𝖼𝗎𝗉 x ↔ ⋃ z = x
74 72 73 anbi12i ⊢ f y 𝖨𝗆𝗀 z ∧ z 𝖡𝗂𝗀𝖼𝗎𝗉 x ↔ z = f y ∧ ⋃ z = x
75 74 exbii ⊢ ∃ z f y 𝖨𝗆𝗀 z ∧ z 𝖡𝗂𝗀𝖼𝗎𝗉 x ↔ ∃ z z = f y ∧ ⋃ z = x
76 12 imaex ⊢ f y ∈ V
77 unieq ⊢ z = f y → ⋃ z = ⋃ f y
78 77 eqeq1d ⊢ z = f y → ⋃ z = x ↔ ⋃ f y = x
79 76 78 ceqsexv ⊢ ∃ z z = f y ∧ ⋃ z = x ↔ ⋃ f y = x
80 eqcom ⊢ ⋃ f y = x ↔ x = ⋃ f y
81 79 80 bitri ⊢ ∃ z z = f y ∧ ⋃ z = x ↔ x = ⋃ f y
82 70 75 81 3bitri ⊢ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 x ↔ x = ⋃ f y
83 68 82 anbi12i ⊢ f y ∈ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∧ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 x ↔ Lim ⁡ y ∧ x = ⋃ f y
84 64 83 bitri ⊢ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 x ↔ Lim ⁡ y ∧ x = ⋃ f y
85 26 brresi ⊢ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ f y ∈ V × ran ⁡ 𝖲𝗎𝖼𝖼 ∧ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x
86 opelxp ⊢ f y ∈ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ f ∈ V ∧ y ∈ ran ⁡ 𝖲𝗎𝖼𝖼
87 12 86 mpbiran ⊢ f y ∈ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ y ∈ ran ⁡ 𝖲𝗎𝖼𝖼
88 39 elrn ⊢ y ∈ ran ⁡ 𝖲𝗎𝖼𝖼 ↔ ∃ z z 𝖲𝗎𝖼𝖼 y
89 71 39 brsuccf ⊢ z 𝖲𝗎𝖼𝖼 y ↔ y = suc ⁡ z
90 89 exbii ⊢ ∃ z z 𝖲𝗎𝖼𝖼 y ↔ ∃ z y = suc ⁡ z
91 87 88 90 3bitri ⊢ f y ∈ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ ∃ z y = suc ⁡ z
92 69 26 brco ⊢ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x ↔ ∃ a f y 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a ∧ a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x
93 vex ⊢ a ∈ V
94 69 93 brco ⊢ f y 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a ↔ ∃ z f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z ∧ z 𝖠𝗉𝗉𝗅𝗒 a
95 12 39 71 brpprod3a ⊢ f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z ↔ ∃ a ∃ b z = a b ∧ f I a ∧ y 𝖡𝗂𝗀𝖼𝗎𝗉 b
96 3anrot ⊢ z = a b ∧ f I a ∧ y 𝖡𝗂𝗀𝖼𝗎𝗉 b ↔ f I a ∧ y 𝖡𝗂𝗀𝖼𝗎𝗉 b ∧ z = a b
97 93 ideq ⊢ f I a ↔ f = a
98 equcom ⊢ f = a ↔ a = f
99 97 98 bitri ⊢ f I a ↔ 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 = a b ↔ z = a b
105 99 103 104 3anbi123i ⊢ f I a ∧ y 𝖡𝗂𝗀𝖼𝗎𝗉 b ∧ z = a b ↔ a = f ∧ b = ⋃ y ∧ z = a b
106 96 105 bitri ⊢ z = a b ∧ f I a ∧ y 𝖡𝗂𝗀𝖼𝗎𝗉 b ↔ a = f ∧ b = ⋃ y ∧ z = a b
107 106 2exbii ⊢ ∃ a ∃ b z = a b ∧ f I a ∧ y 𝖡𝗂𝗀𝖼𝗎𝗉 b ↔ ∃ a ∃ b a = f ∧ b = ⋃ y ∧ z = a b
108 vuniex ⊢ ⋃ y ∈ V
109 opeq1 ⊢ a = f → a b = f b
110 109 eqeq2d ⊢ a = f → z = a b ↔ z = f b
111 opeq2 ⊢ b = ⋃ y → f b = f ⋃ y
112 111 eqeq2d ⊢ b = ⋃ y → z = f b ↔ z = f ⋃ y
113 12 108 110 112 ceqsex2v ⊢ ∃ a ∃ b a = f ∧ b = ⋃ y ∧ z = a b ↔ z = f ⋃ y
114 95 107 113 3bitri ⊢ f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z ↔ z = f ⋃ y
115 114 anbi1i ⊢ f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z ∧ z 𝖠𝗉𝗉𝗅𝗒 a ↔ z = f ⋃ y ∧ z 𝖠𝗉𝗉𝗅𝗒 a
116 115 exbii ⊢ ∃ z f y pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 z ∧ z 𝖠𝗉𝗉𝗅𝗒 a ↔ ∃ z z = f ⋃ y ∧ z 𝖠𝗉𝗉𝗅𝗒 a
117 opex ⊢ f ⋃ y ∈ V
118 breq1 ⊢ z = f ⋃ y → z 𝖠𝗉𝗉𝗅𝗒 a ↔ f ⋃ y 𝖠𝗉𝗉𝗅𝗒 a
119 117 118 ceqsexv ⊢ ∃ z z = f ⋃ y ∧ z 𝖠𝗉𝗉𝗅𝗒 a ↔ f ⋃ y 𝖠𝗉𝗉𝗅𝗒 a
120 12 108 93 brapply ⊢ f ⋃ y 𝖠𝗉𝗉𝗅𝗒 a ↔ a = f ⁡ ⋃ y
121 119 120 bitri ⊢ ∃ z z = f ⋃ y ∧ z 𝖠𝗉𝗉𝗅𝗒 a ↔ a = f ⁡ ⋃ y
122 94 116 121 3bitri ⊢ f y 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a ↔ a = f ⁡ ⋃ y
123 93 26 brfullfun ⊢ a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x ↔ x = F ⁡ a
124 122 123 anbi12i ⊢ f y 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a ∧ a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x ↔ a = f ⁡ ⋃ y ∧ x = F ⁡ a
125 124 exbii ⊢ ∃ a f y 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 a ∧ a 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x ↔ ∃ a a = 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 ⊢ ∃ a a = f ⁡ ⋃ y ∧ x = F ⁡ a ↔ x = F ⁡ f ⁡ ⋃ y
130 92 125 129 3bitri ⊢ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x ↔ x = F ⁡ f ⁡ ⋃ y
131 91 130 anbi12i ⊢ f y ∈ V × ran ⁡ 𝖲𝗎𝖼𝖼 ∧ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 x ↔ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
132 85 131 bitri ⊢ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
133 84 132 orbi12i ⊢ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 x ∨ f y 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
134 63 133 bitri ⊢ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
135 62 134 orbi12i ⊢ f y V × ∅ × ⋃ A x ∨ f y 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
136 54 135 bitri ⊢ f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
137 onzsl ⊢ y ∈ On ↔ y = ∅ ∨ ∃ z ∈ On y = 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 = ⋃ f y
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 = ∅ → ¬ ∃ z y = suc ⁡ z
148 147 intnanrd ⊢ y = ∅ → ¬ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
149 ioran ⊢ ¬ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y ↔ ¬ Lim ⁡ y ∧ x = ⋃ f y ∧ ¬ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
150 141 148 149 sylanbrc ⊢ y = ∅ → ¬ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
151 orel2 ⊢ ¬ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A
152 150 151 syl ⊢ y = ∅ → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A
153 iftrue ⊢ y = ∅ → if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = if A ∈ V A ∅
154 unisnif ⊢ ⋃ A = if A ∈ V A ∅
155 153 154 eqtr4di ⊢ y = ∅ → if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = ⋃ A
156 155 eqeq2d ⊢ y = ∅ → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ x = ⋃ A
157 156 biimprd ⊢ y = ∅ → x = ⋃ A → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
158 157 adantld ⊢ y = ∅ → y = ∅ ∧ x = ⋃ A → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
159 152 158 syld ⊢ y = ∅ → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
160 156 biimpd ⊢ y = ∅ → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → x = ⋃ A
161 160 anc2li ⊢ y = ∅ → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A
162 orc ⊢ y = ∅ ∧ x = ⋃ A → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
163 161 162 syl6 ⊢ y = ∅ → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
164 159 163 impbid ⊢ y = ∅ → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ 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 ∈ On y = suc ⁡ z → ¬ y = ∅ ∧ x = ⋃ A
170 orel1 ⊢ ¬ y = ∅ ∧ x = ⋃ A → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
171 169 170 syl ⊢ ∃ z ∈ On y = suc ⁡ z → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = 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 ∈ On y = suc ⁡ z → ¬ Lim ⁡ y
177 176 intnanrd ⊢ ∃ z ∈ On y = suc ⁡ z → ¬ Lim ⁡ y ∧ x = ⋃ f y
178 orel1 ⊢ ¬ Lim ⁡ y ∧ x = ⋃ f y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
179 177 178 syl ⊢ ∃ z ∈ On y = suc ⁡ z → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
180 142 neii ⊢ ¬ suc ⁡ z = ∅
181 180 iffalsei ⊢ if suc ⁡ z = ∅ if A ∈ V A ∅ if Lim ⁡ suc ⁡ z ⋃ f y F ⁡ f ⁡ ⋃ suc ⁡ z = if Lim ⁡ suc ⁡ z ⋃ f y F ⁡ f ⁡ ⋃ suc ⁡ z
182 iffalse ⊢ ¬ Lim ⁡ suc ⁡ z → if Lim ⁡ suc ⁡ z ⋃ f y F ⁡ f ⁡ ⋃ suc ⁡ z = F ⁡ f ⁡ ⋃ suc ⁡ z
183 71 172 182 mp2b ⊢ if Lim ⁡ suc ⁡ z ⋃ f y F ⁡ f ⁡ ⋃ suc ⁡ z = F ⁡ f ⁡ ⋃ suc ⁡ z
184 181 183 eqtri ⊢ if suc ⁡ z = ∅ if A ∈ V A ∅ if Lim ⁡ suc ⁡ z ⋃ f y F ⁡ 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 → if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = if Lim ⁡ suc ⁡ z ⋃ f y F ⁡ f ⁡ ⋃ suc ⁡ z
190 185 189 ifbieq2d ⊢ y = suc ⁡ z → if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = if suc ⁡ z = ∅ if A ∈ V A ∅ if Lim ⁡ suc ⁡ z ⋃ f y F ⁡ f ⁡ ⋃ suc ⁡ z
191 184 190 188 3eqtr4a ⊢ y = suc ⁡ z → if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = F ⁡ f ⁡ ⋃ y
192 191 rexlimivw ⊢ ∃ z ∈ On y = suc ⁡ z → if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = F ⁡ f ⁡ ⋃ y
193 192 eqeq2d ⊢ ∃ z ∈ On y = suc ⁡ z → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ x = F ⁡ f ⁡ ⋃ y
194 193 biimprd ⊢ ∃ z ∈ On y = suc ⁡ z → x = F ⁡ f ⁡ ⋃ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
195 194 adantld ⊢ ∃ z ∈ On y = suc ⁡ z → ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
196 171 179 195 3syld ⊢ ∃ z ∈ On y = suc ⁡ z → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
197 rexex ⊢ ∃ z ∈ On y = suc ⁡ z → ∃ z y = suc ⁡ z
198 193 biimpd ⊢ ∃ z ∈ On y = suc ⁡ z → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → x = F ⁡ f ⁡ ⋃ y
199 olc ⊢ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
200 199 olcd ⊢ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
201 197 198 200 syl6an ⊢ ∃ z ∈ On y = suc ⁡ z → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
202 196 201 impbid ⊢ ∃ z ∈ On y = suc ⁡ z → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ 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 = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
206 175 exlimiv ⊢ ∃ z y = suc ⁡ z → ¬ Lim ⁡ y
207 206 con2i ⊢ Lim ⁡ y → ¬ ∃ z y = suc ⁡ z
208 207 intnanrd ⊢ Lim ⁡ y → ¬ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
209 orel2 ⊢ ¬ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y
210 208 209 syl ⊢ Lim ⁡ y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y
211 203 iffalsed ⊢ Lim ⁡ y → if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
212 iftrue ⊢ Lim ⁡ y → if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = ⋃ f y
213 211 212 eqtrd ⊢ Lim ⁡ y → if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y = ⋃ f y
214 213 eqeq2d ⊢ Lim ⁡ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ x = ⋃ f y
215 214 biimprd ⊢ Lim ⁡ y → x = ⋃ f y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
216 215 adantld ⊢ Lim ⁡ y → Lim ⁡ y ∧ x = ⋃ f y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
217 205 210 216 3syld ⊢ Lim ⁡ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
218 217 adantl ⊢ y ∈ V ∧ Lim ⁡ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
219 214 biimpd ⊢ Lim ⁡ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → x = ⋃ f y
220 219 anc2li ⊢ Lim ⁡ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → Lim ⁡ y ∧ x = ⋃ f y
221 orc ⊢ Lim ⁡ y ∧ x = ⋃ f y → Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
222 221 olcd ⊢ Lim ⁡ y ∧ x = ⋃ f y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
223 220 222 syl6 ⊢ Lim ⁡ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
224 223 adantl ⊢ y ∈ V ∧ Lim ⁡ y → x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y
225 218 224 impbid ⊢ y ∈ V ∧ Lim ⁡ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
226 164 202 225 3jaoi ⊢ y = ∅ ∨ ∃ z ∈ On y = suc ⁡ z ∨ y ∈ V ∧ Lim ⁡ y → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
227 137 226 sylbi ⊢ y ∈ On → y = ∅ ∧ x = ⋃ A ∨ Lim ⁡ y ∧ x = ⋃ f y ∨ ∃ z y = suc ⁡ z ∧ x = F ⁡ f ⁡ ⋃ y ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
228 136 227 syl5bb ⊢ y ∈ On → f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
229 53 228 syl ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ y ∈ dom ⁡ f → f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
230 26 69 brcnv ⊢ x 𝖠𝗉𝗉𝗅𝗒 -1 f y ↔ f y 𝖠𝗉𝗉𝗅𝗒 x
231 12 39 26 brapply ⊢ f y 𝖠𝗉𝗉𝗅𝗒 x ↔ x = f ⁡ y
232 230 231 bitri ⊢ x 𝖠𝗉𝗉𝗅𝗒 -1 f y ↔ x = f ⁡ y
233 232 a1i ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ y ∈ dom ⁡ f → x 𝖠𝗉𝗉𝗅𝗒 -1 f y ↔ x = f ⁡ y
234 229 233 anbi12d ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ y ∈ dom ⁡ f → f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ∧ x 𝖠𝗉𝗉𝗅𝗒 -1 f y ↔ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ∧ x = f ⁡ y
235 234 biancomd ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ y ∈ dom ⁡ f → f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ∧ x 𝖠𝗉𝗉𝗅𝗒 -1 f y ↔ x = f ⁡ y ∧ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
236 235 exbidv ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ y ∈ dom ⁡ f → ∃ x f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ∧ x 𝖠𝗉𝗉𝗅𝗒 -1 f y ↔ ∃ x x = f ⁡ y ∧ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
237 df-br ⊢ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ f y ∈ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼
238 69 elfix ⊢ f y ∈ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ f y 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 f y
239 69 69 brco ⊢ f y 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 f y ↔ ∃ x f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ∧ x 𝖠𝗉𝗉𝗅𝗒 -1 f y
240 237 238 239 3bitri ⊢ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ ∃ x f y V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 x ∧ x 𝖠𝗉𝗉𝗅𝗒 -1 f y
241 fvex ⊢ f ⁡ y ∈ V
242 241 eqvinc ⊢ f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∃ x x = f ⁡ y ∧ x = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
243 236 240 242 3bitr4g ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ y ∈ dom ⁡ f → f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
244 243 notbid ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ y ∈ dom ⁡ f → ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ ¬ f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
245 244 3expia ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → y ∈ dom ⁡ f → ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ ¬ f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
246 245 pm5.32d ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → y ∈ dom ⁡ f ∧ ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ y ∈ dom ⁡ f ∧ ¬ f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
247 annim ⊢ y ∈ dom ⁡ f ∧ ¬ f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ¬ y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
248 246 247 syl6bb ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → y ∈ dom ⁡ f ∧ ¬ f 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ ¬ y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
249 51 248 syl5bb ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ ¬ y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
250 249 exbidv ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → ∃ y f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y ↔ ∃ y ¬ y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
251 exnal ⊢ ∃ y ¬ y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ¬ ∀ y y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
252 250 251 bitr2di ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → ¬ ∀ y y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∃ y f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y
253 12 eldm ⊢ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ ∃ y f E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 y
254 252 253 bitr4di ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → ¬ ∀ y y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼
255 254 con1bid ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → ¬ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ ∀ y y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
256 df-ral ⊢ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ ∀ y y ∈ dom ⁡ f → f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
257 255 256 bitr4di ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On → ¬ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
258 257 pm5.32i ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ¬ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
259 anass ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
260 258 259 bitri ⊢ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ¬ f ∈ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
261 21 37 260 3bitri ⊢ f ∈ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∖ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ Fun ⁡ f ∧ dom ⁡ f ∈ On ∧ ∀ y ∈ dom ⁡ f f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
262 19 20 261 3bitr4ri ⊢ f ∈ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∖ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 ↔ ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
263 262 abbi2i ⊢ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∖ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
264 263 unieqi ⊢ ⋃ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∖ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼 = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = if y = ∅ if A ∈ V A ∅ if Lim ⁡ y ⋃ f y F ⁡ f ⁡ ⋃ y
265 1 264 eqtr4i ⊢ rec ⁡ F A = ⋃ 𝖥𝗎𝗇𝗌 ∩ 𝖣𝗈𝗆𝖺𝗂𝗇 -1 On ∖ dom ⁡ E -1 ∘ 𝖣𝗈𝗆𝖺𝗂𝗇 ∖ 𝖥𝗂𝗑 𝖠𝗉𝗉𝗅𝗒 -1 ∘ V × ∅ × ⋃ A ∪ 𝖡𝗂𝗀𝖼𝗎𝗉 ∘ 𝖨𝗆𝗀 ↾ V × 𝖫𝗂𝗆𝗂𝗍𝗌 ∪ 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F ∘ 𝖠𝗉𝗉𝗅𝗒 ∘ pprod I 𝖡𝗂𝗀𝖼𝗎𝗉 ↾ V × ran ⁡ 𝖲𝗎𝖼𝖼