Theorem dfrdg4 33407

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.)

Assertion

Ref	Expression
dfrdg4	⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))))

Proof of Theorem dfrdg4

Dummy variables 𝑎 𝑏 𝑓 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfrdg3 33036	. 2 ⊢ rec(𝐹, 𝐴) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
2		an12 643	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
3		df-fn 6353	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4		ancom 463	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5		eqcom 2828	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓)
6	5	anbi1i 625	. . . . . . . . . 10 ⊢ ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7	3, 4, 6	3bitri 299	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
8	7	anbi1i 625	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
9		anass 471	. . . . . . . 8 ⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
10	2, 8, 9	3bitri 299	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
11	10	exbii 1844	. . . . . 6 ⊢ (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
12		vex 3498	. . . . . . . 8 ⊢ 𝑓 ∈ V
13	12	dmex 7610	. . . . . . 7 ⊢ dom 𝑓 ∈ V
14		eleq1 2900	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15		raleq 3406	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
16	14, 15	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
17	16	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
18	13, 17	ceqsexv 3542	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
19	11, 18	bitri 277	. . . . 5 ⊢ (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
20		df-rex 3144	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
21		eldif 3946	. . . . . 6 ⊢ (𝑓 ∈ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))))
22		elin 4169	. . . . . . . 8 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)))
23	12	elfuns 33371	. . . . . . . . 9 ⊢ (𝑓 ∈ Funs ↔ Fun 𝑓)
24	12	elima 5929	. . . . . . . . . 10 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓)
25		df-rex 3144	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On 𝑥◡Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓))
26		vex 3498	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
27	26, 12	brcnv 5748	. . . . . . . . . . . . . 14 ⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥)
28	12, 26	brdomain 33389	. . . . . . . . . . . . . 14 ⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
29	27, 28	bitri 277	. . . . . . . . . . . . 13 ⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
30	29	anbi1ci 627	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ (𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
31	30	exbii 1844	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
32	13, 14	ceqsexv 3542	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
33	31, 32	bitri 277	. . . . . . . . . 10 ⊢ (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ dom 𝑓 ∈ On)
34	24, 25, 33	3bitri 299	. . . . . . . . 9 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On)
35	23, 34	anbi12i 628	. . . . . . . 8 ⊢ ((𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
36	22, 35	bitri 277	. . . . . . 7 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
37	36	anbi1i 625	. . . . . 6 ⊢ ((𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))))
38		brdif 5112	. . . . . . . . . . . . . . 15 ⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ (𝑓(◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦))
39		vex 3498	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑦 ∈ V
40	12, 39	brco 5736	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦))
41	28	anbi1i 625	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
42	41	exbii 1844	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
43		breq1 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = dom 𝑓 → (𝑥◡ E 𝑦 ↔ dom 𝑓◡ E 𝑦))
44	13, 43	ceqsexv 3542	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
45	42, 44	bitri 277	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
46	13, 39	brcnv 5748	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
47	13	epeli 5463	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓)
48	46, 47	bitri 277	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓)
49	40, 45, 48	3bitri 299	. . . . . . . . . . . . . . . 16 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓)
50	49	anbi1i 625	. . . . . . . . . . . . . . 15 ⊢ ((𝑓(◡ E ∘ Domain)𝑦 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦))
51	38, 50	bitri 277	. . . . . . . . . . . . . 14 ⊢ (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦))
52		onelon 6211	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
53	52	3adant1 1126	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
54		brun 5110	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥))
55		brxp 5596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}))
56		opelxp 5586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
57	12, 56	mpbiran 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
58		velsn 4577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
59	57, 58	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
60		velsn 4577	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ {∪ {𝐴}} ↔ 𝑥 = ∪ {𝐴})
61	59, 60	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
62	55, 61	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
63		brun 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥))
64	26	brresi 5857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥))
65		opelxp 5586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ Limits ))
66	12, 65	mpbiran 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 ∈ Limits )
67	39	ellimits 33366	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ Limits ↔ Lim 𝑦)
68	66, 67	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
69		opex 5349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ⟨𝑓, 𝑦⟩ ∈ V
70	69, 26	brco 5736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥))
71		vex 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑧 ∈ V
72	12, 39, 71	brimg 33393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟨𝑓, 𝑦⟩Img𝑧 ↔ 𝑧 = (𝑓 “ 𝑦))
73	26	brbigcup 33354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 Bigcup 𝑥 ↔ ∪ 𝑧 = 𝑥)
74	72, 73	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
75	74	exbii 1844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
76	12	imaex 7615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 “ 𝑦) ∈ V
77		unieq 4840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑦) → ∪ 𝑧 = ∪ (𝑓 “ 𝑦))
78	77	eqeq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑦) → (∪ 𝑧 = 𝑥 ↔ ∪ (𝑓 “ 𝑦) = 𝑥))
79	76, 78	ceqsexv 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ ∪ (𝑓 “ 𝑦) = 𝑥)
80		eqcom 2828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∪ (𝑓 “ 𝑦) = 𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
81	79, 80	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
82	70, 75, 81	3bitri 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
83	68, 82	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥) ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
84	64, 83	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
85	26	brresi 5857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥))
86		opelxp 5586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
87	12, 86	mpbiran 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
88	39	elrn 5817	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
89	71, 39	brsuccf 33397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧Succ𝑦 ↔ 𝑦 = suc 𝑧)
90	89	exbii 1844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
91	87, 88, 90	3bitri 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
92	69, 26	brco 5736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥))
93		vex 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑎 ∈ V
94	69, 93	brco 5736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎))
95	12, 39, 71	brpprod3a 33342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏))
96		3anrot 1096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
97	93	ideq 5718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓 I 𝑎 ↔ 𝑓 = 𝑎)
98		equcom 2021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓 = 𝑎 ↔ 𝑎 = 𝑓)
99	97, 98	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑓 I 𝑎 ↔ 𝑎 = 𝑓)
100		vex 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ 𝑏 ∈ V
101	100	brbigcup 33354	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑦 Bigcup 𝑏 ↔ ∪ 𝑦 = 𝑏)
102		eqcom 2828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (∪ 𝑦 = 𝑏 ↔ 𝑏 = ∪ 𝑦)
103	101, 102	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑦 Bigcup 𝑏 ↔ 𝑏 = ∪ 𝑦)
104		biid 263	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
105	99, 103, 104	3anbi123i 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
106	96, 105	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
107	106	2exbii 1845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
108		vuniex 7459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ∪ 𝑦 ∈ V
109		opeq1 4797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
110	109	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
111		opeq2 4798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 = ∪ 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, ∪ 𝑦⟩)
112	111	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 = ∪ 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩))
113	12, 108, 110, 112	ceqsex2v 3545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
114	95, 107, 113	3bitri 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
115	114	anbi1i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
116	115	exbii 1844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
117		opex 5349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ⟨𝑓, ∪ 𝑦⟩ ∈ V
118		breq1 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 = ⟨𝑓, ∪ 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎))
119	117, 118	ceqsexv 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎)
120	12, 108, 93	brapply 33394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑓, ∪ 𝑦⟩Apply𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
121	119, 120	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓‘∪ 𝑦))
122	94, 116, 121	3bitri 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
123	93, 26	brfullfun 33404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎FullFun𝐹𝑥 ↔ 𝑥 = (𝐹‘𝑎))
124	122, 123	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
125	124	exbii 1844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
126		fvex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓‘∪ 𝑦) ∈ V
127		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝐹‘𝑎) = (𝐹‘(𝑓‘∪ 𝑦)))
128	127	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝑥 = (𝐹‘𝑎) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
129	126, 128	ceqsexv 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))
130	92, 125, 129	3bitri 299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))
131	91, 130	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥) ↔ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
132	85, 131	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
133	84, 132	orbi12i 911	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
134	63, 133	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
135	62, 134	orbi12i 911	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥) ↔ ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
136	54, 135	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
137		onzsl 7555	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
138		nlim0 6244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ¬ Lim ∅
139		limeq 6198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
140	138, 139	mtbiri 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → ¬ Lim 𝑦)
141	140	intnanrd 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
142		nsuceq0 6266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ suc 𝑧 ≠ ∅
143		neeq2 3079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = ∅ → (suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅))
144	142, 143	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = ∅ → suc 𝑧 ≠ 𝑦)
145	144	necomd 3071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
146	145	neneqd 3021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
147	146	nexdv 1933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
148	147	intnanrd 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
149		ioran 980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
150	141, 148, 149	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → ¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
151		orel2 887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
153		iftrue 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
154		unisnif 33381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
155	153, 154	syl6eqr 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ {𝐴})
156	155	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ {𝐴}))
157	156	biimprd 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → (𝑥 = ∪ {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
158	157	adantld 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
159	152, 158	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
160	156	biimpd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ {𝐴}))
161	160	anc2li 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
162		orc 863	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
163	161, 162	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
164	159, 163	impbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
165		neeq1 3078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
166	142, 165	mpbiri 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → 𝑦 ≠ ∅)
167	166	neneqd 3021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
168	167	intnanrd 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
169	168	rexlimivw 3282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
170		orel1 885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
172		nlimsucg 7551	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ V → ¬ Lim suc 𝑧)
173	172	elv 3500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ¬ Lim suc 𝑧
174		limeq 6198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
175	173, 174	mtbiri 329	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
176	175	rexlimivw 3282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
177	176	intnanrd 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
178		orel1 885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
179	177, 178	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
180	142	neii 3018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ¬ suc 𝑧 = ∅
181	180	iffalsei 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))
182		iffalse 4476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)))
183	71, 172, 182	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))
184	181, 183	eqtri 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧))
185		eqeq1 2825	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
186		unieq 4840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧)
187	186	fveq2d 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧))
188	187	fveq2d 6669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
189	174, 188	ifbieq2d 4492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))
190	185, 189	ifbieq2d 4492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
191	184, 190, 188	3eqtr4a 2882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
192	191	rexlimivw 3282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
193	192	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
194	193	biimprd 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓‘∪ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
195	194	adantld 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
196	171, 179, 195	3syld 60	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
197		rexex 3240	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
198	193	biimpd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
199		olc 864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
200	199	olcd 870	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
201	197, 198, 200	syl6an 682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
202	196, 201	impbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
203	140	con2i 141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → ¬ 𝑦 = ∅)
204	203	intnanrd 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
205	204, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
206	175	exlimiv 1927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
207	206	con2i 141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
208	207	intnanrd 492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
209		orel2 887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
210	208, 209	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
211	203	iffalsed 4478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
212		iftrue 4473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
213	211, 212	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ (𝑓 “ 𝑦))
214	213	eqeq2d 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ (𝑓 “ 𝑦)))
215	214	biimprd 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → (𝑥 = ∪ (𝑓 “ 𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
216	215	adantld 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
217	205, 210, 216	3syld 60	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
218	217	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
219	214	biimpd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ (𝑓 “ 𝑦)))
220	219	anc2li 558	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
221		orc 863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
222	221	olcd 870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
223	220, 222	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
224	223	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
225	218, 224	impbid 214	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
226	164, 202, 225	3jaoi 1423	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
227	137, 226	sylbi 219	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
228	136, 227	syl5bb 285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ On → (⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
229	53, 228	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
230	26, 69	brcnv 5748	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
231	12, 39, 26	brapply 33394	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑓, 𝑦⟩Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦))
232	230, 231	bitri 277	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦))
233	232	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦)))
234	229, 233	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ∧ 𝑥 = (𝑓‘𝑦))))
235	234	biancomd 466	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → ((⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ (𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
236	235	exbidv 1918	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (∃𝑥(⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
237		df-br 5060	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ⟨𝑓, 𝑦⟩ ∈ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))
238	69	elfix 33359	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑓, 𝑦⟩ ∈ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))) ↔ ⟨𝑓, 𝑦⟩(◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))⟨𝑓, 𝑦⟩)
239	69, 69	brco 5736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑓, 𝑦⟩(◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))⟨𝑓, 𝑦⟩ ↔ ∃𝑥(⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩))
240	237, 238, 239	3bitri 299	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ∃𝑥(⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ∧ 𝑥◡Apply⟨𝑓, 𝑦⟩))
241		fvex 6678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓‘𝑦) ∈ V
242	241	eqvinc 3642	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
243	236, 240, 242	3bitr4g 316	. . . . . . . . . . . . . . . . . 18 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
244	243	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
245	244	3expia 1117	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (𝑦 ∈ dom 𝑓 → (¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦 ↔ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
246	245	pm5.32d 579	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → ((𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦) ↔ (𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
247		annim 406	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
248	246, 247	syl6bb 289	. . . . . . . . . . . . . 14 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → ((𝑦 ∈ dom 𝑓 ∧ ¬ 𝑓 Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))𝑦) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
249	51, 248	syl5bb 285	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
250	249	exbidv 1918	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦 ↔ ∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
251		exnal 1823	. . . . . . . . . . . 12 ⊢ (∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
252	250, 251	syl6rbb 290	. . . . . . . . . . 11 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦))
253	12	eldm 5764	. . . . . . . . . . 11 ⊢ (𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))) ↔ ∃𝑦 𝑓((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))𝑦)
254	252, 253	syl6bbr 291	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))))
255	254	con1bid 358	. . . . . . . . 9 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
256		df-ral 3143	. . . . . . . . 9 ⊢ (∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
257	255, 256	syl6bbr 291	. . . . . . . 8 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) → (¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
258	257	pm5.32i 577	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ ((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
259		anass 471	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
260	258, 259	bitri 277	. . . . . 6 ⊢ (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ¬ 𝑓 ∈ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
261	21, 37, 260	3bitri 299	. . . . 5 ⊢ (𝑓 ∈ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
262	19, 20, 261	3bitr4ri 306	. . . 4 ⊢ (𝑓 ∈ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
263	262	abbi2i 2953	. . 3 ⊢ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
264	263	unieqi 4841	. 2 ⊢ ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))))) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
265	1, 264	eqtr4i 2847	1 ⊢ rec(𝐹, 𝐴) = ∪ (( Funs ∩ (◡Domain “ On)) ∖ dom ((◡ E ∘ Domain) ∖ Fix (◡Apply ∘ (((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   ∨ w3o 1082   ∧ w3a 1083  ∀wal 1531   = wceq 1533  ∃wex 1776   ∈ wcel 2110  {cab 2799   ≠ wne 3016  ∀wral 3138  ∃wrex 3139  Vcvv 3495   ∖ cdif 3933   ∪ cun 3934   ∩ cin 3935  ∅c0 4291  ifcif 4467  {csn 4561  ⟨cop 4567  ∪ cuni 4832   class class class wbr 5059   I cid 5454   E cep 5459   × cxp 5548  ^◡ccnv 5549  dom cdm 5550  ran crn 5551   ↾ cres 5552   “ cima 5553   ∘ ccom 5554  Oncon0 6186  Lim wlim 6187  suc csuc 6188  Fun wfun 6344   Fn wfn 6345  ‘cfv 6350  reccrdg 8039  pprodcpprod 33287   Bigcup cbigcup 33290   Fix cfix 33291   Limits climits 33292   Funs cfuns 33293  Imgcimg 33298  Domaincdomain 33299  Applycapply 33301  Succcsuccf 33304  FullFuncfullfn 33306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-symdif 4219  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-txp 33310  df-pprod 33311  df-bigcup 33314  df-fix 33315  df-limits 33316  df-funs 33317  df-singleton 33318  df-singles 33319  df-image 33320  df-cart 33321  df-img 33322  df-domain 33323  df-cup 33325  df-succf 33328  df-apply 33329  df-funpart 33330  df-fullfun 33331

This theorem is referenced by: (None)