Theorem dfrdg4 35225

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 35070	. 2 ⊢ rec(𝐹, 𝐴) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}
2		an12 641	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
3		df-fn 6547	. . . . . . . . . 10 ⊢ (𝑓 Fn 𝑥 ↔ (Fun 𝑓 ∧ dom 𝑓 = 𝑥))
4		ancom 459	. . . . . . . . . 10 ⊢ ((Fun 𝑓 ∧ dom 𝑓 = 𝑥) ↔ (dom 𝑓 = 𝑥 ∧ Fun 𝑓))
5		eqcom 2737	. . . . . . . . . . 11 ⊢ (dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓)
6	5	anbi1i 622	. . . . . . . . . 10 ⊢ ((dom 𝑓 = 𝑥 ∧ Fun 𝑓) ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
7	3, 4, 6	3bitri 296	. . . . . . . . 9 ⊢ (𝑓 Fn 𝑥 ↔ (𝑥 = dom 𝑓 ∧ Fun 𝑓))
8	7	anbi1i 622	. . . . . . . 8 ⊢ ((𝑓 Fn 𝑥 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ ((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
9		anass 467	. . . . . . . 8 ⊢ (((𝑥 = dom 𝑓 ∧ Fun 𝑓) ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
10	2, 8, 9	3bitri 296	. . . . . . 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 3476	. . . . . . . 8 ⊢ 𝑓 ∈ V
13	12	dmex 7906	. . . . . . 7 ⊢ dom 𝑓 ∈ V
14		eleq1 2819	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (𝑥 ∈ On ↔ dom 𝑓 ∈ On))
15		raleq 3320	. . . . . . . . 9 ⊢ (𝑥 = dom 𝑓 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
16	14, 15	anbi12d 629	. . . . . . . 8 ⊢ (𝑥 = dom 𝑓 → ((𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
17	16	anbi2d 627	. . . . . . 7 ⊢ (𝑥 = dom 𝑓 → ((Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))))
18	13, 17	ceqsexv 3524	. . . . . 6 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ (Fun 𝑓 ∧ (𝑥 ∈ On ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
19	11, 18	bitri 274	. . . . 5 ⊢ (∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
20		df-rex 3069	. . . . 5 ⊢ (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ∃𝑥(𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
21		eldif 3959	. . . . . 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 3965	. . . . . . . 8 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)))
23	12	elfuns 35189	. . . . . . . . 9 ⊢ (𝑓 ∈ Funs ↔ Fun 𝑓)
24	12	elima 6065	. . . . . . . . . 10 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ ∃𝑥 ∈ On 𝑥◡Domain𝑓)
25		df-rex 3069	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On 𝑥◡Domain𝑓 ↔ ∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓))
26		vex 3476	. . . . . . . . . . . . . . 15 ⊢ 𝑥 ∈ V
27	26, 12	brcnv 5883	. . . . . . . . . . . . . 14 ⊢ (𝑥◡Domain𝑓 ↔ 𝑓Domain𝑥)
28	12, 26	brdomain 35207	. . . . . . . . . . . . . 14 ⊢ (𝑓Domain𝑥 ↔ 𝑥 = dom 𝑓)
29	27, 28	bitri 274	. . . . . . . . . . . . 13 ⊢ (𝑥◡Domain𝑓 ↔ 𝑥 = dom 𝑓)
30	29	anbi1ci 624	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ (𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
31	30	exbii 1848	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On))
32	13, 14	ceqsexv 3524	. . . . . . . . . . 11 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥 ∈ On) ↔ dom 𝑓 ∈ On)
33	31, 32	bitri 274	. . . . . . . . . 10 ⊢ (∃𝑥(𝑥 ∈ On ∧ 𝑥◡Domain𝑓) ↔ dom 𝑓 ∈ On)
34	24, 25, 33	3bitri 296	. . . . . . . . 9 ⊢ (𝑓 ∈ (◡Domain “ On) ↔ dom 𝑓 ∈ On)
35	23, 34	anbi12i 625	. . . . . . . 8 ⊢ ((𝑓 ∈ Funs ∧ 𝑓 ∈ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
36	22, 35	bitri 274	. . . . . . 7 ⊢ (𝑓 ∈ ( Funs ∩ (◡Domain “ On)) ↔ (Fun 𝑓 ∧ dom 𝑓 ∈ On))
37	36	anbi1i 622	. . . . . 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 5202	. . . . . . . . . . . . . . 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 3476	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑦 ∈ V
40	12, 39	brco 5871	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ ∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦))
41	28	anbi1i 622	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ (𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
42	41	exbii 1848	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ ∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦))
43		breq1 5152	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = dom 𝑓 → (𝑥◡ E 𝑦 ↔ dom 𝑓◡ E 𝑦))
44	13, 43	ceqsexv 3524	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑥(𝑥 = dom 𝑓 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
45	42, 44	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑥(𝑓Domain𝑥 ∧ 𝑥◡ E 𝑦) ↔ dom 𝑓◡ E 𝑦)
46	13, 39	brcnv 5883	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 E dom 𝑓)
47	13	epeli 5583	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓)
48	46, 47	bitri 274	. . . . . . . . . . . . . . . . 17 ⊢ (dom 𝑓◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓)
49	40, 45, 48	3bitri 296	. . . . . . . . . . . . . . . 16 ⊢ (𝑓(◡ E ∘ Domain)𝑦 ↔ 𝑦 ∈ dom 𝑓)
50	49	anbi1i 622	. . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . 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 6390	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
53	52	3adant1 1128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → 𝑦 ∈ On)
54		brun 5200	. . . . . . . . . . . . . . . . . . . . . . . . 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 5726	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}))
56		opelxp 5713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ {∅}))
57	12, 56	mpbiran 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 ∈ {∅})
58		velsn 4645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 ∈ {∅} ↔ 𝑦 = ∅)
59	57, 58	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ↔ 𝑦 = ∅)
60		velsn 4645	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑥 ∈ {∪ {𝐴}} ↔ 𝑥 = ∪ {𝐴})
61	59, 60	anbi12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × {∅}) ∧ 𝑥 ∈ {∪ {𝐴}}) ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
62	55, 61	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (⟨𝑓, 𝑦⟩((V × {∅}) × {∪ {𝐴}})𝑥 ↔ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
63		brun 5200	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 5991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥))
65		opelxp 5713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ Limits ))
66	12, 65	mpbiran 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ 𝑦 ∈ Limits )
67	39	ellimits 35184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ Limits ↔ Lim 𝑦)
68	66, 67	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ↔ Lim 𝑦)
69		opex 5465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ⟨𝑓, 𝑦⟩ ∈ V
70	69, 26	brco 5871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ ∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥))
71		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑧 ∈ V
72	12, 39, 71	brimg 35211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟨𝑓, 𝑦⟩Img𝑧 ↔ 𝑧 = (𝑓 “ 𝑦))
73	26	brbigcup 35172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 Bigcup 𝑥 ↔ ∪ 𝑧 = 𝑥)
74	72, 73	anbi12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ (𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
75	74	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧(⟨𝑓, 𝑦⟩Img𝑧 ∧ 𝑧 Bigcup 𝑥) ↔ ∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥))
76	12	imaex 7911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 “ 𝑦) ∈ V
77		unieq 4920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝑓 “ 𝑦) → ∪ 𝑧 = ∪ (𝑓 “ 𝑦))
78	77	eqeq1d 2732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 = (𝑓 “ 𝑦) → (∪ 𝑧 = 𝑥 ↔ ∪ (𝑓 “ 𝑦) = 𝑥))
79	76, 78	ceqsexv 3524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ ∪ (𝑓 “ 𝑦) = 𝑥)
80		eqcom 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∪ (𝑓 “ 𝑦) = 𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
81	79, 80	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧(𝑧 = (𝑓 “ 𝑦) ∧ ∪ 𝑧 = 𝑥) ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
82	70, 75, 81	3bitri 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥 ↔ 𝑥 = ∪ (𝑓 “ 𝑦))
83	68, 82	anbi12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × Limits ) ∧ ⟨𝑓, 𝑦⟩( Bigcup ∘ Img)𝑥) ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
84	64, 83	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑓, 𝑦⟩(( Bigcup ∘ Img) ↾ (V × Limits ))𝑥 ↔ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
85	26	brresi 5991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (⟨𝑓, 𝑦⟩((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))𝑥 ↔ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥))
86		opelxp 5713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ (𝑓 ∈ V ∧ 𝑦 ∈ ran Succ))
87	12, 86	mpbiran 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ 𝑦 ∈ ran Succ)
88	39	elrn 5894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 ∈ ran Succ ↔ ∃𝑧 𝑧Succ𝑦)
89	71, 39	brsuccf 35215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧Succ𝑦 ↔ 𝑦 = suc 𝑧)
90	89	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧 𝑧Succ𝑦 ↔ ∃𝑧 𝑦 = suc 𝑧)
91	87, 88, 90	3bitri 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ↔ ∃𝑧 𝑦 = suc 𝑧)
92	69, 26	brco 5871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ ∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥))
93		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ 𝑎 ∈ V
94	69, 93	brco 5871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ ∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎))
95	12, 39, 71	brpprod3a 35160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ ∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏))
96		3anrot 1098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
97	93	ideq 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓 I 𝑎 ↔ 𝑓 = 𝑎)
98		equcom 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑓 = 𝑎 ↔ 𝑎 = 𝑓)
99	97, 98	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑓 I 𝑎 ↔ 𝑎 = 𝑓)
100		vex 3476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ 𝑏 ∈ V
101	100	brbigcup 35172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑦 Bigcup 𝑏 ↔ ∪ 𝑦 = 𝑏)
102		eqcom 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (∪ 𝑦 = 𝑏 ↔ 𝑏 = ∪ 𝑦)
103	101, 102	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑦 Bigcup 𝑏 ↔ 𝑏 = ∪ 𝑦)
104		biid 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑎, 𝑏⟩)
105	99, 103, 104	3anbi123i 1153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
106	96, 105	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ (𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
107	106	2exbii 1849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∃𝑎∃𝑏(𝑧 = ⟨𝑎, 𝑏⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩))
108		vuniex 7733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ∪ 𝑦 ∈ V
109		opeq1 4874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑎 = 𝑓 → ⟨𝑎, 𝑏⟩ = ⟨𝑓, 𝑏⟩)
110	109	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑎 = 𝑓 → (𝑧 = ⟨𝑎, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, 𝑏⟩))
111		opeq2 4875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑏 = ∪ 𝑦 → ⟨𝑓, 𝑏⟩ = ⟨𝑓, ∪ 𝑦⟩)
112	111	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑏 = ∪ 𝑦 → (𝑧 = ⟨𝑓, 𝑏⟩ ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩))
113	12, 108, 110, 112	ceqsex2v 3529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (∃𝑎∃𝑏(𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨𝑎, 𝑏⟩) ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
114	95, 107, 113	3bitri 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ↔ 𝑧 = ⟨𝑓, ∪ 𝑦⟩)
115	114	anbi1i 622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ (𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
116	115	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑧(⟨𝑓, 𝑦⟩pprod( I , Bigcup )𝑧 ∧ 𝑧Apply𝑎) ↔ ∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎))
117		opex 5465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ⟨𝑓, ∪ 𝑦⟩ ∈ V
118		breq1 5152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 = ⟨𝑓, ∪ 𝑦⟩ → (𝑧Apply𝑎 ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎))
119	117, 118	ceqsexv 3524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ ⟨𝑓, ∪ 𝑦⟩Apply𝑎)
120	12, 108, 93	brapply 35212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (⟨𝑓, ∪ 𝑦⟩Apply𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
121	119, 120	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∃𝑧(𝑧 = ⟨𝑓, ∪ 𝑦⟩ ∧ 𝑧Apply𝑎) ↔ 𝑎 = (𝑓‘∪ 𝑦))
122	94, 116, 121	3bitri 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ↔ 𝑎 = (𝑓‘∪ 𝑦))
123	93, 26	brfullfun 35222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎FullFun𝐹𝑥 ↔ 𝑥 = (𝐹‘𝑎))
124	122, 123	anbi12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ (𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
125	124	exbii 1848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑎(⟨𝑓, 𝑦⟩(Apply ∘ pprod( I , Bigcup ))𝑎 ∧ 𝑎FullFun𝐹𝑥) ↔ ∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)))
126		fvex 6905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓‘∪ 𝑦) ∈ V
127		fveq2 6892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝐹‘𝑎) = (𝐹‘(𝑓‘∪ 𝑦)))
128	127	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = (𝑓‘∪ 𝑦) → (𝑥 = (𝐹‘𝑎) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
129	126, 128	ceqsexv 3524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑎(𝑎 = (𝑓‘∪ 𝑦) ∧ 𝑥 = (𝐹‘𝑎)) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))
130	92, 125, 129	3bitri 296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥 ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))
131	91, 130	anbi12i 625	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((⟨𝑓, 𝑦⟩ ∈ (V × ran Succ) ∧ ⟨𝑓, 𝑦⟩(FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup )))𝑥) ↔ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
132	85, 131	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . . . . . . . . . . . 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 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑓, 𝑦⟩(((V × {∅}) × {∪ {𝐴}}) ∪ ((( Bigcup ∘ Img) ↾ (V × Limits )) ∪ ((FullFun𝐹 ∘ (Apply ∘ pprod( I , Bigcup ))) ↾ (V × ran Succ))))𝑥 ↔ ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
137		onzsl 7839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ On ↔ (𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)))
138		nlim0 6424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ¬ Lim ∅
139		limeq 6377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → (Lim 𝑦 ↔ Lim ∅))
140	138, 139	mtbiri 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → ¬ Lim 𝑦)
141	140	intnanrd 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → ¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)))
142		nsuceq0 6448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ suc 𝑧 ≠ ∅
143		neeq2 3002	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = ∅ → (suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅))
144	142, 143	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = ∅ → suc 𝑧 ≠ 𝑦)
145	144	necomd 2994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = ∅ → 𝑦 ≠ suc 𝑧)
146	145	neneqd 2943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → ¬ 𝑦 = suc 𝑧)
147	146	nexdv 1937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → ¬ ∃𝑧 𝑦 = suc 𝑧)
148	147	intnanrd 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
149		ioran 980	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) ↔ (¬ (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∧ ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
150	141, 148, 149	sylanbrc 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → ¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))
151		orel2 887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (¬ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴})))
153		iftrue 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(𝐴 ∈ V, 𝐴, ∅))
154		unisnif 35199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ∪ {𝐴} = if(𝐴 ∈ V, 𝐴, ∅)
155	153, 154	eqtr4di 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = ∅ → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ {𝐴})
156	155	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ {𝐴}))
157	156	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → (𝑥 = ∪ {𝐴} → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
158	157	adantld 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
159	152, 158	syld 47	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
160	156	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑦 = ∅ → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ {𝐴}))
161	160	anc2li 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = ∅ → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
165		neeq1 3001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = suc 𝑧 → (𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅))
166	142, 165	mpbiri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → 𝑦 ≠ ∅)
167	166	neneqd 2943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = suc 𝑧 → ¬ 𝑦 = ∅)
168	167	intnanrd 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑦 = suc 𝑧 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
169	168	rexlimivw 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑧 ∈ V → ¬ Lim suc 𝑧)
173	172	elv 3478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ¬ Lim suc 𝑧
174		limeq 6377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → (Lim 𝑦 ↔ Lim suc 𝑧))
175	173, 174	mtbiri 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑦 = suc 𝑧 → ¬ Lim 𝑦)
176	175	rexlimivw 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
177	176	intnanrd 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ¬ suc 𝑧 = ∅
181	180	iffalsei 4539	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))
182		iffalse 4538	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (¬ Lim suc 𝑧 → if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧)))
183	71, 172, 182	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))) = (𝐹‘(𝑓‘∪ suc 𝑧))
184	181, 183	eqtri 2758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))) = (𝐹‘(𝑓‘∪ suc 𝑧))
185		eqeq1 2734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = suc 𝑧 → (𝑦 = ∅ ↔ suc 𝑧 = ∅))
186		unieq 4920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧)
187	186	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑦 = suc 𝑧 → (𝑓‘∪ 𝑦) = (𝑓‘∪ suc 𝑧))
188	187	fveq2d 6896	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑦 = suc 𝑧 → (𝐹‘(𝑓‘∪ 𝑦)) = (𝐹‘(𝑓‘∪ suc 𝑧)))
189	174, 188	ifbieq2d 4555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑦 = suc 𝑧 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧))))
190	185, 189	ifbieq2d 4555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(suc 𝑧 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim suc 𝑧, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ suc 𝑧)))))
191	184, 190, 188	3eqtr4a 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
192	191	rexlimivw 3149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = (𝐹‘(𝑓‘∪ 𝑦)))
193	192	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
194	193	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = (𝐹‘(𝑓‘∪ 𝑦)) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
195	194	adantld 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3074	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → ∃𝑧 𝑦 = suc 𝑧)
198	193	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 680	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
202	196, 201	impbid 211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∃𝑧 ∈ On 𝑦 = suc 𝑧 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
203	140	con2i 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → ¬ 𝑦 = ∅)
204	203	intnanrd 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → ¬ (𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}))
205	204, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))))
206	175	exlimiv 1931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (∃𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦)
207	206	con2i 139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → ¬ ∃𝑧 𝑦 = suc 𝑧)
208	207	intnanrd 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → ¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))
209		orel2 887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (¬ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))) → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
210	208, 209	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (Lim 𝑦 → (((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))) → (Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦))))
211	203	iffalsed 4540	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))
212		iftrue 4535	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (Lim 𝑦 → if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))) = ∪ (𝑓 “ 𝑦))
213	211, 212	eqtrd 2770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (Lim 𝑦 → if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) = ∪ (𝑓 “ 𝑦))
214	213	eqeq2d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ 𝑥 = ∪ (𝑓 “ 𝑦)))
215	214	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → (𝑥 = ∪ (𝑓 “ 𝑦) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
216	215	adantld 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) → 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
219	214	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (Lim 𝑦 → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → 𝑥 = ∪ (𝑓 “ 𝑦)))
220	219	anc2li 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) → ((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦)))))))
225	218, 224	impbid 211	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑦 ∈ V ∧ Lim 𝑦) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
226	164, 202, 225	3jaoi 1425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 = ∅ ∨ ∃𝑧 ∈ On 𝑦 = suc 𝑧 ∨ (𝑦 ∈ V ∧ Lim 𝑦)) → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
227	137, 226	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ On → (((𝑦 = ∅ ∧ 𝑥 = ∪ {𝐴}) ∨ ((Lim 𝑦 ∧ 𝑥 = ∪ (𝑓 “ 𝑦)) ∨ (∃𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = (𝐹‘(𝑓‘∪ 𝑦))))) ↔ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
228	136, 227	bitrid 282	. . . . . . . . . . . . . . . . . . . . . . 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 5883	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ ⟨𝑓, 𝑦⟩Apply𝑥)
231	12, 39, 26	brapply 35212	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑓, 𝑦⟩Apply𝑥 ↔ 𝑥 = (𝑓‘𝑦))
232	230, 231	bitri 274	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦))
233	232	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓) → (𝑥◡Apply⟨𝑓, 𝑦⟩ ↔ 𝑥 = (𝑓‘𝑦)))
234	229, 233	anbi12d 629	. . . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . 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 1922	. . . . . . . . . . . . . . . . . . 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 5150	. . . . . . . . . . . . . . . . . . . 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 35177	. . . . . . . . . . . . . . . . . . . 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 5871	. . . . . . . . . . . . . . . . . . . 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 296	. . . . . . . . . . . . . . . . . . 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 6905	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓‘𝑦) ∈ V
242	241	eqvinc 3638	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∃𝑥(𝑥 = (𝑓‘𝑦) ∧ 𝑥 = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
243	236, 240, 242	3bitr4g 313	. . . . . . . . . . . . . . . . . 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 317	. . . . . . . . . . . . . . . . 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 1119	. . . . . . . . . . . . . . . 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 575	. . . . . . . . . . . . . . 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 402	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ dom 𝑓 ∧ ¬ (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ ¬ (𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
248	246, 247	bitrdi 286	. . . . . . . . . . . . . 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 282	. . . . . . . . . . . . 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 1922	. . . . . . . . . . . 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 287	. . . . . . . . . . 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 5901	. . . . . . . . . . 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 288	. . . . . . . . . 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 354	. . . . . . . . 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 3060	. . . . . . . . 9 ⊢ (∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))) ↔ ∀𝑦(𝑦 ∈ dom 𝑓 → (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))))
257	255, 256	bitr4di 288	. . . . . . . 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 573	. . . . . . 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 467	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ dom 𝑓 ∈ On) ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦))))) ↔ (Fun 𝑓 ∧ (dom 𝑓 ∈ On ∧ ∀𝑦 ∈ dom 𝑓(𝑓‘𝑦) = if(𝑦 = ∅, if(𝐴 ∈ V, 𝐴, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))))
260	258, 259	bitri 274	. . . . . 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 296	. . . . 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 303	. . . 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 2867	. . 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 4922	. 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 2761	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 205   ∧ wa 394   ∨ wo 843   ∨ w3o 1084   ∧ w3a 1085  ∀wal 1537   = wceq 1539  ∃wex 1779   ∈ wcel 2104  {cab 2707   ≠ wne 2938  ∀wral 3059  ∃wrex 3068  Vcvv 3472   ∖ cdif 3946   ∪ cun 3947   ∩ cin 3948  ∅c0 4323  ifcif 4529  {csn 4629  ⟨cop 4635  ∪ cuni 4909   class class class wbr 5149   I cid 5574   E cep 5580   × cxp 5675  ^◡ccnv 5676  dom cdm 5677  ran crn 5678   ↾ cres 5679   “ cima 5680   ∘ ccom 5681  Oncon0 6365  Lim wlim 6366  suc csuc 6367  Fun wfun 6538   Fn wfn 6539  ‘cfv 6544  reccrdg 8413  pprodcpprod 35105   Bigcup cbigcup 35108   Fix cfix 35109   Limits climits 35110   Funs cfuns 35111  Imgcimg 35116  Domaincdomain 35117  Applycapply 35119  Succcsuccf 35122  FullFuncfullfn 35124

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-symdif 4243  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-txp 35128  df-pprod 35129  df-bigcup 35132  df-fix 35133  df-limits 35134  df-funs 35135  df-singleton 35136  df-singles 35137  df-image 35138  df-cart 35139  df-img 35140  df-domain 35141  df-cup 35143  df-succf 35146  df-apply 35147  df-funpart 35148  df-fullfun 35149

This theorem is referenced by: (None)