Theorem dfrdg4 35939

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 35784	. 2 ⊢ rec(𝐹, 𝐴) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
2		an12 645	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
3		df-fn 6514	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4		ancom 460	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5		eqcom 2736	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓)
6	5	anbi1i 624	. . . . . . . . . 10 ⊢ ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7	3, 4, 6	3bitri 297	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
8	7	anbi1i 624	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
9		anass 468	. . . . . . . 8 ⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
10	2, 8, 9	3bitri 297	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
11	10	exbii 1848	. . . . . 6 ⊢ (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
12		vex 3451	. . . . . . . 8 ⊢ 𝑓 ∈ V
13	12	dmex 7885	. . . . . . 7 ⊢ dom 𝑓 ∈ V
14		eleq1 2816	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15		raleq 3296	. . . . . . . . 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 3498	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
19	11, 18	bitri 275	. . . . 5 ⊢ (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
20		df-rex 3054	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
21		eldif 3924	. . . . . 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 3930	. . . . . . . 8 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)))
23	12	elfuns 35903	. . . . . . . . 9 ⊢ (𝑓 ∈ Funs ↔ Fun 𝑓)
24	12	elima 6036	. . . . . . . . . 10 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓)
25		df-rex 3054	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On 𝑥◡Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓))
26		vex 3451	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
27	26, 12	brcnv 5846	. . . . . . . . . . . . . 14 ⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥)
28	12, 26	brdomain 35921	. . . . . . . . . . . . . 14 ⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
29	27, 28	bitri 275	. . . . . . . . . . . . 13 ⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
30	29	anbi1ci 626	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ (𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
31	30	exbii 1848	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
32	13, 14	ceqsexv 3498	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
33	31, 32	bitri 275	. . . . . . . . . 10 ⊢ (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ dom 𝑓 ∈ On)
34	24, 25, 33	3bitri 297	. . . . . . . . 9 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On)
35	23, 34	anbi12i 628	. . . . . . . 8 ⊢ ((𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
36	22, 35	bitri 275	. . . . . . 7 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
37	36	anbi1i 624	. . . . . 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 5160	. . . . . . . . . . . . . . 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 3451	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑦 ∈ V
40	12, 39	brco 5834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦))
41	28	anbi1i 624	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
42	41	exbii 1848	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
43		breq1 5110	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = dom 𝑓 → (𝑥◡ E 𝑦 ↔ dom 𝑓◡ E 𝑦))
44	13, 43	ceqsexv 3498	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
45	42, 44	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
46	13, 39	brcnv 5846	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
47	13	epeli 5540	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓)
48	46, 47	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓)
49	40, 45, 48	3bitri 297	. . . . . . . . . . . . . . . 16 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓)
50	49	anbi1i 624	. . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . . 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 6357	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
53	52	3adant1 1130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
54		brun 5158	. . . . . . . . . . . . . . . . . . . . . . . . 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 5687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}))
56		opelxp 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
57	12, 56	mpbiran 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
58		velsn 4605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
59	57, 58	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
60		velsn 4605	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ {∪ {𝐴}} ↔ 𝑥 = ∪ {𝐴})
61	59, 60	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
62	55, 61	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
63		brun 5158	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥))
65		opelxp 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ Limits ))
66	12, 65	mpbiran 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 ∈ Limits )
67	39	ellimits 35898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ Limits ↔ Lim 𝑦)
68	66, 67	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
69		opex 5424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ⟨𝑓, 𝑦⟩ ∈ V
70	69, 26	brco 5834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥))
71		vex 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑧 ∈ V
72	12, 39, 71	brimg 35925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟨𝑓, 𝑦⟩Img𝑧 ↔ 𝑧 = (𝑓 “ 𝑦))
73	26	brbigcup 35886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 Bigcup 𝑥 ↔ ∪ 𝑧 = 𝑥)
74	72, 73	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
75	74	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
76	12	imaex 7890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 “ 𝑦) ∈ V
77		unieq 4882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑦) → ∪ 𝑧 = ∪ (𝑓 “ 𝑦))
78	77	eqeq1d 2731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑦) → (∪ 𝑧 = 𝑥 ↔ ∪ (𝑓 “ 𝑦) = 𝑥))
79	76, 78	ceqsexv 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ ∪ (𝑓 “ 𝑦) = 𝑥)
80		eqcom 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∪ (𝑓 “ 𝑦) = 𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
81	79, 80	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
82	70, 75, 81	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
83	68, 82	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥) ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
84	64, 83	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
85	26	brresi 5959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥))
86		opelxp 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
87	12, 86	mpbiran 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
88	39	elrn 5857	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
89	71, 39	brsuccf 35929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧Succ𝑦 ↔ 𝑦 = suc 𝑧)
90	89	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
91	87, 88, 90	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
92	69, 26	brco 5834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥))
93		vex 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑎 ∈ V
94	69, 93	brco 5834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎))
95	12, 39, 71	brpprod3a 35874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏))
96		3anrot 1099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
97	93	ideq 5816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓 I 𝑎 ↔ 𝑓 = 𝑎)
98		equcom 2018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓 = 𝑎 ↔ 𝑎 = 𝑓)
99	97, 98	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑓 I 𝑎 ↔ 𝑎 = 𝑓)
100		vex 3451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ 𝑏 ∈ V
101	100	brbigcup 35886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑦 Bigcup 𝑏 ↔ ∪ 𝑦 = 𝑏)
102		eqcom 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (∪ 𝑦 = 𝑏 ↔ 𝑏 = ∪ 𝑦)
103	101, 102	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑦 Bigcup 𝑏 ↔ 𝑏 = ∪ 𝑦)
104		biid 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
105	99, 103, 104	3anbi123i 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
106	96, 105	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
107	106	2exbii 1849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
108		vuniex 7715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ∪ 𝑦 ∈ V
109		opeq1 4837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
110	109	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
111		opeq2 4838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 = ∪ 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, ∪ 𝑦⟩)
112	111	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 = ∪ 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩))
113	12, 108, 110, 112	ceqsex2v 3502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
114	95, 107, 113	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
115	114	anbi1i 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
116	115	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
117		opex 5424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ⟨𝑓, ∪ 𝑦⟩ ∈ V
118		breq1 5110	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 = ⟨𝑓, ∪ 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎))
119	117, 118	ceqsexv 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎)
120	12, 108, 93	brapply 35926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑓, ∪ 𝑦⟩Apply𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
121	119, 120	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓‘∪ 𝑦))
122	94, 116, 121	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
123	93, 26	brfullfun 35936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎FullFun𝐹𝑥 ↔ 𝑥 = (𝐹‘𝑎))
124	122, 123	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
125	124	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
126		fvex 6871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓‘∪ 𝑦) ∈ V
127		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝐹‘𝑎) = (𝐹‘(𝑓‘∪ 𝑦)))
128	127	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝑥 = (𝐹‘𝑎) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
129	126, 128	ceqsexv 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))
130	92, 125, 129	3bitri 297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
133	84, 132	orbi12i 914	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ∨ ⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥) ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
134	63, 133	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥 ↔ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
135	62, 134	orbi12i 914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ∨ ⟨𝑓, 𝑦⟩((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ)))𝑥) ↔ ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
136	54, 135	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
137		onzsl 7822	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
138		nlim0 6392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ¬ Lim ∅
139		limeq 6344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
140	138, 139	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → ¬ Lim 𝑦)
141	140	intnanrd 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
142		nsuceq0 6417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ suc 𝑧 ≠ ∅
143		neeq2 2988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = ∅ → (suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅))
144	142, 143	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = ∅ → suc 𝑧 ≠ 𝑦)
145	144	necomd 2980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
146	145	neneqd 2930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
147	146	nexdv 1936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
148	147	intnanrd 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
149		ioran 985	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
150	141, 148, 149	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → ¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
151		orel2 890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
153		iftrue 4494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
154		unisnif 35913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
155	153, 154	eqtr4di 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ {𝐴})
156	155	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ {𝐴}))
157	156	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → (𝑥 = ∪ {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
158	157	adantld 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
159	152, 158	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
160	156	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ {𝐴}))
161	160	anc2li 555	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
162		orc 867	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
163	161, 162	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
164	159, 163	impbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
165		neeq1 2987	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
166	142, 165	mpbiri 258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → 𝑦 ≠ ∅)
167	166	neneqd 2930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
168	167	intnanrd 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
169	168	rexlimivw 3130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
170		orel1 888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
171	169, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
172		nlimsucg 7818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ V → ¬ Lim suc 𝑧)
173	172	elv 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ¬ Lim suc 𝑧
174		limeq 6344	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
175	173, 174	mtbiri 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
176	175	rexlimivw 3130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
177	176	intnanrd 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
178		orel1 888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
179	177, 178	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
180	142	neii 2927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ¬ suc 𝑧 = ∅
181	180	iffalsei 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))
182		iffalse 4497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)))
183	71, 172, 182	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))
184	181, 183	eqtri 2752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧))
185		eqeq1 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
186		unieq 4882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧)
187	186	fveq2d 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧))
188	187	fveq2d 6862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
189	174, 188	ifbieq2d 4515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))
190	185, 189	ifbieq2d 4515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
191	184, 190, 188	3eqtr4a 2790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
192	191	rexlimivw 3130	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
193	192	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
194	193	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓‘∪ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
195	194	adantld 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3059	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
198	193	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
199		olc 868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
200	199	olcd 874	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
201	197, 198, 200	syl6an 684	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
202	196, 201	impbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
203	140	con2i 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → ¬ 𝑦 = ∅)
204	203	intnanrd 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
205	204, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
206	175	exlimiv 1930	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
207	206	con2i 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
208	207	intnanrd 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
209		orel2 890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
210	208, 209	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
211	203	iffalsed 4499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
212		iftrue 4494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
213	211, 212	eqtrd 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ (𝑓 “ 𝑦))
214	213	eqeq2d 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ (𝑓 “ 𝑦)))
215	214	biimprd 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → (𝑥 = ∪ (𝑓 “ 𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
216	215	adantld 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
219	214	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ (𝑓 “ 𝑦)))
220	219	anc2li 555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
221		orc 867	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
222	221	olcd 874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
223	220, 222	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
224	223	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
225	218, 224	impbid 212	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
226	164, 202, 225	3jaoi 1430	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
227	137, 226	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
228	136, 227	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . 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 5846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
231	12, 39, 26	brapply 35926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑓, 𝑦⟩Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦))
232	230, 231	bitri 275	. . . . . . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . . . . 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 1921	. . . . . . . . . . . . . . . . . . 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 5108	. . . . . . . . . . . . . . . . . . . 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 35891	. . . . . . . . . . . . . . . . . . . 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 5834	. . . . . . . . . . . . . . . . . . . 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 297	. . . . . . . . . . . . . . . . . . 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 6871	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓‘𝑦) ∈ V
242	241	eqvinc 3615	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
243	236, 240, 242	3bitr4g 314	. . . . . . . . . . . . . . . . . 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 318	. . . . . . . . . . . . . . . . 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 1121	. . . . . . . . . . . . . . . 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 577	. . . . . . . . . . . . . . 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 403	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
248	246, 247	bitrdi 287	. . . . . . . . . . . . . 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	bitrid 283	. . . . . . . . . . . . 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 1921	. . . . . . . . . . . 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 1827	. . . . . . . . . . . 12 ⊢ (∃𝑦 ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
252	250, 251	bitr2di 288	. . . . . . . . . . 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 5864	. . . . . . . . . . 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	bitr4di 289	. . . . . . . . . 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 355	. . . . . . . . 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 3045	. . . . . . . . 9 ⊢ (∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
257	255, 256	bitr4di 289	. . . . . . . 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 574	. . . . . . 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 468	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
260	258, 259	bitri 275	. . . . . 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 297	. . . . 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 304	. . . 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	eqabi 2863	. . 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 4883	. 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 2755	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 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913  ∅c0 4296  ifcif 4488  {csn 4589  ⟨cop 4595  ∪ cuni 4871   class class class wbr 5107   I cid 5532   E cep 5537   × cxp 5636  ^◡ccnv 5637  dom cdm 5638  ran crn 5639   ↾ cres 5640   “ cima 5641   ∘ ccom 5642  Oncon0 6332  Lim wlim 6333  suc csuc 6334  Fun wfun 6505   Fn wfn 6506  ‘cfv 6511  reccrdg 8377  pprodcpprod 35819   Bigcup cbigcup 35822   Fix cfix 35823   Limits climits 35824   Funs cfuns 35825  Imgcimg 35830  Domaincdomain 35831  Applycapply 35833  Succcsuccf 35836  FullFuncfullfn 35838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-symdif 4216  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-txp 35842  df-pprod 35843  df-bigcup 35846  df-fix 35847  df-limits 35848  df-funs 35849  df-singleton 35850  df-singles 35851  df-image 35852  df-cart 35853  df-img 35854  df-domain 35855  df-cup 35857  df-succf 35860  df-apply 35861  df-funpart 35862  df-fullfun 35863

This theorem is referenced by: (None)