dfrdg4

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

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

Proof

Step	Hyp	Ref	Expression
1		dfrdg3	⊢ rec ( 𝐹 , 𝐴 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) }
2		an12	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
3		df-fn	⊢ ( 𝑓 Fn 𝑥 ↔ ( Fun 𝑓 ∧ dom 𝑓 = 𝑥 ) )
4		ancom	⊢ ( ( Fun 𝑓 ∧ dom 𝑓 = 𝑥 ) ↔ ( dom 𝑓 = 𝑥 ∧ Fun 𝑓 ) )
5		eqcom	⊢ ( dom 𝑓 = 𝑥 ↔ 𝑥 = dom 𝑓 )
6	5	anbi1i	⊢ ( ( dom 𝑓 = 𝑥 ∧ Fun 𝑓 ) ↔ ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) )
7	3 4 6	3bitri	⊢ ( 𝑓 Fn 𝑥 ↔ ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) )
8	7	anbi1i	⊢ ( ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
9		anass	⊢ ( ( ( 𝑥 = dom 𝑓 ∧ Fun 𝑓 ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) )
10	2 8 9	3bitri	⊢ ( ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) )
11	10	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) )
12		vex	⊢ 𝑓 ∈ V
13	12	dmex	⊢ dom 𝑓 ∈ V
14		eleq1	⊢ ( 𝑥 = dom 𝑓 → ( 𝑥 ∈ On ↔ dom 𝑓 ∈ On ) )
15		raleq	⊢ ( 𝑥 = dom 𝑓 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
16	14 15	anbi12d	⊢ ( 𝑥 = dom 𝑓 → ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
17	16	anbi2d	⊢ ( 𝑥 = dom 𝑓 → ( ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) )
18	13 17	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ ( Fun 𝑓 ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
19	11 18	bitri	⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
20		df-rex	⊢ ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
21		eldif	⊢ ( 𝑓 ∈ ( ( 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	⊢ ( 𝑓 ∈ ( Funs ∩ ( ^◡ Domain “ On ) ) ↔ ( 𝑓 ∈ Funs ∧ 𝑓 ∈ ( ^◡ Domain “ On ) ) )
23	12	elfuns	⊢ ( 𝑓 ∈ Funs ↔ Fun 𝑓 )
24	12	elima	⊢ ( 𝑓 ∈ ( ^◡ Domain “ On ) ↔ ∃ 𝑥 ∈ On 𝑥 ^◡ Domain 𝑓 )
25		df-rex	⊢ ( ∃ 𝑥 ∈ On 𝑥 ^◡ Domain 𝑓 ↔ ∃ 𝑥 ( 𝑥 ∈ On ∧ 𝑥 ^◡ Domain 𝑓 ) )
26		vex	⊢ 𝑥 ∈ V
27	26 12	brcnv	⊢ ( 𝑥 ^◡ Domain 𝑓 ↔ 𝑓 Domain 𝑥 )
28	12 26	brdomain	⊢ ( 𝑓 Domain 𝑥 ↔ 𝑥 = dom 𝑓 )
29	27 28	bitri	⊢ ( 𝑥 ^◡ Domain 𝑓 ↔ 𝑥 = dom 𝑓 )
30	29	anbi1ci	⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ^◡ Domain 𝑓 ) ↔ ( 𝑥 = dom 𝑓 ∧ 𝑥 ∈ On ) )
31	30	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ 𝑥 ^◡ Domain 𝑓 ) ↔ ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ∈ On ) )
32	13 14	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ∈ On ) ↔ dom 𝑓 ∈ On )
33	31 32	bitri	⊢ ( ∃ 𝑥 ( 𝑥 ∈ On ∧ 𝑥 ^◡ Domain 𝑓 ) ↔ dom 𝑓 ∈ On )
34	24 25 33	3bitri	⊢ ( 𝑓 ∈ ( ^◡ Domain “ On ) ↔ dom 𝑓 ∈ On )
35	23 34	anbi12i	⊢ ( ( 𝑓 ∈ Funs ∧ 𝑓 ∈ ( ^◡ Domain “ On ) ) ↔ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) )
36	22 35	bitri	⊢ ( 𝑓 ∈ ( Funs ∩ ( ^◡ Domain “ On ) ) ↔ ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) )
37	36	anbi1i	⊢ ( ( 𝑓 ∈ ( 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	⊢ ( 𝑓 ( ( ^◡ 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	⊢ 𝑦 ∈ V
40	12 39	brco	⊢ ( 𝑓 ( ^◡ E ∘ Domain ) 𝑦 ↔ ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ^◡ E 𝑦 ) )
41	28	anbi1i	⊢ ( ( 𝑓 Domain 𝑥 ∧ 𝑥 ^◡ E 𝑦 ) ↔ ( 𝑥 = dom 𝑓 ∧ 𝑥 ^◡ E 𝑦 ) )
42	41	exbii	⊢ ( ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ^◡ E 𝑦 ) ↔ ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ^◡ E 𝑦 ) )
43		breq1	⊢ ( 𝑥 = dom 𝑓 → ( 𝑥 ^◡ E 𝑦 ↔ dom 𝑓 ^◡ E 𝑦 ) )
44	13 43	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = dom 𝑓 ∧ 𝑥 ^◡ E 𝑦 ) ↔ dom 𝑓 ^◡ E 𝑦 )
45	42 44	bitri	⊢ ( ∃ 𝑥 ( 𝑓 Domain 𝑥 ∧ 𝑥 ^◡ E 𝑦 ) ↔ dom 𝑓 ^◡ E 𝑦 )
46	13 39	brcnv	⊢ ( dom 𝑓 ^◡ E 𝑦 ↔ 𝑦 E dom 𝑓 )
47	13	epeli	⊢ ( 𝑦 E dom 𝑓 ↔ 𝑦 ∈ dom 𝑓 )
48	46 47	bitri	⊢ ( dom 𝑓 ^◡ E 𝑦 ↔ 𝑦 ∈ dom 𝑓 )
49	40 45 48	3bitri	⊢ ( 𝑓 ( ^◡ E ∘ Domain ) 𝑦 ↔ 𝑦 ∈ dom 𝑓 )
50	49	anbi1i	⊢ ( ( 𝑓 ( ^◡ 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	⊢ ( 𝑓 ( ( ^◡ 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	⊢ ( ( dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓 ) → 𝑦 ∈ On )
53	52	3adant1	⊢ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓 ) → 𝑦 ∈ On )
54		brun	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( 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	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) 𝑥 ↔ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ∧ 𝑥 ∈ { ∪ { 𝐴 } } ) )
56		opelxp	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ↔ ( 𝑓 ∈ V ∧ 𝑦 ∈ { ∅ } ) )
57	12 56	mpbiran	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ↔ 𝑦 ∈ { ∅ } )
58		velsn	⊢ ( 𝑦 ∈ { ∅ } ↔ 𝑦 = ∅ )
59	57 58	bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ↔ 𝑦 = ∅ )
60		velsn	⊢ ( 𝑥 ∈ { ∪ { 𝐴 } } ↔ 𝑥 = ∪ { 𝐴 } )
61	59 60	anbi12i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × { ∅ } ) ∧ 𝑥 ∈ { ∪ { 𝐴 } } ) ↔ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) )
62	55 61	bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) 𝑥 ↔ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) )
63		brun	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( 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	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) 𝑥 ↔ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ) )
65		opelxp	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ↔ ( 𝑓 ∈ V ∧ 𝑦 ∈ Limits ) )
66	12 65	mpbiran	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ↔ 𝑦 ∈ Limits )
67	39	ellimits	⊢ ( 𝑦 ∈ Limits ↔ Lim 𝑦 )
68	66 67	bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ↔ Lim 𝑦 )
69		opex	⊢ ⟨ 𝑓 , 𝑦 ⟩ ∈ V
70	69 26	brco	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ↔ ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ∧ 𝑧 Bigcup 𝑥 ) )
71		vex	⊢ 𝑧 ∈ V
72	12 39 71	brimg	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ↔ 𝑧 = ( 𝑓 “ 𝑦 ) )
73	26	brbigcup	⊢ ( 𝑧 Bigcup 𝑥 ↔ ∪ 𝑧 = 𝑥 )
74	72 73	anbi12i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ∧ 𝑧 Bigcup 𝑥 ) ↔ ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) )
75	74	exbii	⊢ ( ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ Img 𝑧 ∧ 𝑧 Bigcup 𝑥 ) ↔ ∃ 𝑧 ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) )
76	12	imaex	⊢ ( 𝑓 “ 𝑦 ) ∈ V
77		unieq	⊢ ( 𝑧 = ( 𝑓 “ 𝑦 ) → ∪ 𝑧 = ∪ ( 𝑓 “ 𝑦 ) )
78	77	eqeq1d	⊢ ( 𝑧 = ( 𝑓 “ 𝑦 ) → ( ∪ 𝑧 = 𝑥 ↔ ∪ ( 𝑓 “ 𝑦 ) = 𝑥 ) )
79	76 78	ceqsexv	⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) ↔ ∪ ( 𝑓 “ 𝑦 ) = 𝑥 )
80		eqcom	⊢ ( ∪ ( 𝑓 “ 𝑦 ) = 𝑥 ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) )
81	79 80	bitri	⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝑓 “ 𝑦 ) ∧ ∪ 𝑧 = 𝑥 ) ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) )
82	70 75 81	3bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) )
83	68 82	anbi12i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × Limits ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( Bigcup ∘ Img ) 𝑥 ) ↔ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) )
84	64 83	bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) 𝑥 ↔ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) )
85	26	brresi	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) 𝑥 ↔ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ) )
86		opelxp	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ↔ ( 𝑓 ∈ V ∧ 𝑦 ∈ ran Succ ) )
87	12 86	mpbiran	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ↔ 𝑦 ∈ ran Succ )
88	39	elrn	⊢ ( 𝑦 ∈ ran Succ ↔ ∃ 𝑧 𝑧 Succ 𝑦 )
89	71 39	brsuccf	⊢ ( 𝑧 Succ 𝑦 ↔ 𝑦 = suc 𝑧 )
90	89	exbii	⊢ ( ∃ 𝑧 𝑧 Succ 𝑦 ↔ ∃ 𝑧 𝑦 = suc 𝑧 )
91	87 88 90	3bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ↔ ∃ 𝑧 𝑦 = suc 𝑧 )
92	69 26	brco	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ↔ ∃ 𝑎 ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ∧ 𝑎 FullFun 𝐹 𝑥 ) )
93		vex	⊢ 𝑎 ∈ V
94	69 93	brco	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ↔ ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ∧ 𝑧 Apply 𝑎 ) )
95	12 39 71	brpprod3a	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) )
96		3anrot	⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) ↔ ( 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
97	93	ideq	⊢ ( 𝑓 I 𝑎 ↔ 𝑓 = 𝑎 )
98		equcom	⊢ ( 𝑓 = 𝑎 ↔ 𝑎 = 𝑓 )
99	97 98	bitri	⊢ ( 𝑓 I 𝑎 ↔ 𝑎 = 𝑓 )
100		vex	⊢ 𝑏 ∈ V
101	100	brbigcup	⊢ ( 𝑦 Bigcup 𝑏 ↔ ∪ 𝑦 = 𝑏 )
102		eqcom	⊢ ( ∪ 𝑦 = 𝑏 ↔ 𝑏 = ∪ 𝑦 )
103	101 102	bitri	⊢ ( 𝑦 Bigcup 𝑏 ↔ 𝑏 = ∪ 𝑦 )
104		biid	⊢ ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ )
105	99 103 104	3anbi123i	⊢ ( ( 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
106	96 105	bitri	⊢ ( ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) ↔ ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
107	106	2exbii	⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑓 I 𝑎 ∧ 𝑦 Bigcup 𝑏 ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) )
108		vuniex	⊢ ∪ 𝑦 ∈ V
109		opeq1	⊢ ( 𝑎 = 𝑓 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑓 , 𝑏 ⟩ )
110	109	eqeq2d	⊢ ( 𝑎 = 𝑓 → ( 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝑓 , 𝑏 ⟩ ) )
111		opeq2	⊢ ( 𝑏 = ∪ 𝑦 → ⟨ 𝑓 , 𝑏 ⟩ = ⟨ 𝑓 , ∪ 𝑦 ⟩ )
112	111	eqeq2d	⊢ ( 𝑏 = ∪ 𝑦 → ( 𝑧 = ⟨ 𝑓 , 𝑏 ⟩ ↔ 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ) )
113	12 108 110 112	ceqsex2v	⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 = 𝑓 ∧ 𝑏 = ∪ 𝑦 ∧ 𝑧 = ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ )
114	95 107 113	3bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ↔ 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ )
115	114	anbi1i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ∧ 𝑧 Apply 𝑎 ) ↔ ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) )
116	115	exbii	⊢ ( ∃ 𝑧 ( ⟨ 𝑓 , 𝑦 ⟩ pprod ( I , Bigcup ) 𝑧 ∧ 𝑧 Apply 𝑎 ) ↔ ∃ 𝑧 ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) )
117		opex	⊢ ⟨ 𝑓 , ∪ 𝑦 ⟩ ∈ V
118		breq1	⊢ ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ → ( 𝑧 Apply 𝑎 ↔ ⟨ 𝑓 , ∪ 𝑦 ⟩ Apply 𝑎 ) )
119	117 118	ceqsexv	⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) ↔ ⟨ 𝑓 , ∪ 𝑦 ⟩ Apply 𝑎 )
120	12 108 93	brapply	⊢ ( ⟨ 𝑓 , ∪ 𝑦 ⟩ Apply 𝑎 ↔ 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) )
121	119 120	bitri	⊢ ( ∃ 𝑧 ( 𝑧 = ⟨ 𝑓 , ∪ 𝑦 ⟩ ∧ 𝑧 Apply 𝑎 ) ↔ 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) )
122	94 116 121	3bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ↔ 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) )
123	93 26	brfullfun	⊢ ( 𝑎 FullFun 𝐹 𝑥 ↔ 𝑥 = ( 𝐹 ‘ 𝑎 ) )
124	122 123	anbi12i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ∧ 𝑎 FullFun 𝐹 𝑥 ) ↔ ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) )
125	124	exbii	⊢ ( ∃ 𝑎 ( ⟨ 𝑓 , 𝑦 ⟩ ( Apply ∘ pprod ( I , Bigcup ) ) 𝑎 ∧ 𝑎 FullFun 𝐹 𝑥 ) ↔ ∃ 𝑎 ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) )
126		fvex	⊢ ( 𝑓 ‘ ∪ 𝑦 ) ∈ V
127		fveq2	⊢ ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) )
128	127	eqeq2d	⊢ ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) → ( 𝑥 = ( 𝐹 ‘ 𝑎 ) ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
129	126 128	ceqsexv	⊢ ( ∃ 𝑎 ( 𝑎 = ( 𝑓 ‘ ∪ 𝑦 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑎 ) ) ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) )
130	92 125 129	3bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) )
131	91 130	anbi12i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ∈ ( V × ran Succ ) ∧ ⟨ 𝑓 , 𝑦 ⟩ ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) 𝑥 ) ↔ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
132	85 131	bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) 𝑥 ↔ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
133	84 132	orbi12i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) 𝑥 ∨ ⟨ 𝑓 , 𝑦 ⟩ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) 𝑥 ) ↔ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
134	63 133	bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) 𝑥 ↔ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
135	62 134	orbi12i	⊢ ( ( ⟨ 𝑓 , 𝑦 ⟩ ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) 𝑥 ∨ ⟨ 𝑓 , 𝑦 ⟩ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) 𝑥 ) ↔ ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
136	54 135	bitri	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) ∪ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) ) 𝑥 ↔ ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
137		onzsl	⊢ ( 𝑦 ∈ On ↔ ( 𝑦 = ∅ ∨ ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 ∨ ( 𝑦 ∈ V ∧ Lim 𝑦 ) ) )
138		nlim0	⊢ ¬ Lim ∅
139		limeq	⊢ ( 𝑦 = ∅ → ( Lim 𝑦 ↔ Lim ∅ ) )
140	138 139	mtbiri	⊢ ( 𝑦 = ∅ → ¬ Lim 𝑦 )
141	140	intnanrd	⊢ ( 𝑦 = ∅ → ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) )
142		nsuceq0	⊢ suc 𝑧 ≠ ∅
143		neeq2	⊢ ( 𝑦 = ∅ → ( suc 𝑧 ≠ 𝑦 ↔ suc 𝑧 ≠ ∅ ) )
144	142 143	mpbiri	⊢ ( 𝑦 = ∅ → suc 𝑧 ≠ 𝑦 )
145	144	necomd	⊢ ( 𝑦 = ∅ → 𝑦 ≠ suc 𝑧 )
146	145	neneqd	⊢ ( 𝑦 = ∅ → ¬ 𝑦 = suc 𝑧 )
147	146	nexdv	⊢ ( 𝑦 = ∅ → ¬ ∃ 𝑧 𝑦 = suc 𝑧 )
148	147	intnanrd	⊢ ( 𝑦 = ∅ → ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
149		ioran	⊢ ( ¬ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ( ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∧ ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
150	141 148 149	sylanbrc	⊢ ( 𝑦 = ∅ → ¬ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
151		orel2	⊢ ( ¬ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) )
152	150 151	syl	⊢ ( 𝑦 = ∅ → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) )
153		iftrue	⊢ ( 𝑦 = ∅ → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( 𝐴 ∈ V , 𝐴 , ∅ ) )
154		unisnif	⊢ ∪ { 𝐴 } = if ( 𝐴 ∈ V , 𝐴 , ∅ )
155	153 154	eqtr4di	⊢ ( 𝑦 = ∅ → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ∪ { 𝐴 } )
156	155	eqeq2d	⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ 𝑥 = ∪ { 𝐴 } ) )
157	156	biimprd	⊢ ( 𝑦 = ∅ → ( 𝑥 = ∪ { 𝐴 } → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
158	157	adantld	⊢ ( 𝑦 = ∅ → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
159	152 158	syld	⊢ ( 𝑦 = ∅ → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
160	156	biimpd	⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → 𝑥 = ∪ { 𝐴 } ) )
161	160	anc2li	⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ) )
162		orc	⊢ ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
163	161 162	syl6	⊢ ( 𝑦 = ∅ → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
164	159 163	impbid	⊢ ( 𝑦 = ∅ → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
165		neeq1	⊢ ( 𝑦 = suc 𝑧 → ( 𝑦 ≠ ∅ ↔ suc 𝑧 ≠ ∅ ) )
166	142 165	mpbiri	⊢ ( 𝑦 = suc 𝑧 → 𝑦 ≠ ∅ )
167	166	neneqd	⊢ ( 𝑦 = suc 𝑧 → ¬ 𝑦 = ∅ )
168	167	intnanrd	⊢ ( 𝑦 = suc 𝑧 → ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) )
169	168	rexlimivw	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) )
170		orel1	⊢ ( ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
171	169 170	syl	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
172		nlimsucg	⊢ ( 𝑧 ∈ V → ¬ Lim suc 𝑧 )
173	172	elv	⊢ ¬ Lim suc 𝑧
174		limeq	⊢ ( 𝑦 = suc 𝑧 → ( Lim 𝑦 ↔ Lim suc 𝑧 ) )
175	173 174	mtbiri	⊢ ( 𝑦 = suc 𝑧 → ¬ Lim 𝑦 )
176	175	rexlimivw	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ Lim 𝑦 )
177	176	intnanrd	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) )
178		orel1	⊢ ( ¬ ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
179	177 178	syl	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
180	142	neii	⊢ ¬ suc 𝑧 = ∅
181	180	iffalsei	⊢ if ( suc 𝑧 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) )
182		iffalse	⊢ ( ¬ Lim suc 𝑧 → if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) )
183	71 172 182	mp2b	⊢ if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) )
184	181 183	eqtri	⊢ if ( suc 𝑧 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) )
185		eqeq1	⊢ ( 𝑦 = suc 𝑧 → ( 𝑦 = ∅ ↔ suc 𝑧 = ∅ ) )
186		unieq	⊢ ( 𝑦 = suc 𝑧 → ∪ 𝑦 = ∪ suc 𝑧 )
187	186	fveq2d	⊢ ( 𝑦 = suc 𝑧 → ( 𝑓 ‘ ∪ 𝑦 ) = ( 𝑓 ‘ ∪ suc 𝑧 ) )
188	187	fveq2d	⊢ ( 𝑦 = suc 𝑧 → ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) )
189	174 188	ifbieq2d	⊢ ( 𝑦 = suc 𝑧 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) = if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) )
190	185 189	ifbieq2d	⊢ ( 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( suc 𝑧 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim suc 𝑧 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ suc 𝑧 ) ) ) ) )
191	184 190 188	3eqtr4a	⊢ ( 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) )
192	191	rexlimivw	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) )
193	192	eqeq2d	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
194	193	biimprd	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
195	194	adantld	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
196	171 179 195	3syld	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
197		rexex	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ∃ 𝑧 𝑦 = suc 𝑧 )
198	193	biimpd	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
199		olc	⊢ ( ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
200	199	olcd	⊢ ( ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
201	197 198 200	syl6an	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
202	196 201	impbid	⊢ ( ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
203	140	con2i	⊢ ( Lim 𝑦 → ¬ 𝑦 = ∅ )
204	203	intnanrd	⊢ ( Lim 𝑦 → ¬ ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) )
205	204 170	syl	⊢ ( Lim 𝑦 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
206	175	exlimiv	⊢ ( ∃ 𝑧 𝑦 = suc 𝑧 → ¬ Lim 𝑦 )
207	206	con2i	⊢ ( Lim 𝑦 → ¬ ∃ 𝑧 𝑦 = suc 𝑧 )
208	207	intnanrd	⊢ ( Lim 𝑦 → ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
209		orel2	⊢ ( ¬ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) )
210	208 209	syl	⊢ ( Lim 𝑦 → ( ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) )
211	203	iffalsed	⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) )
212		iftrue	⊢ ( Lim 𝑦 → if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) = ∪ ( 𝑓 “ 𝑦 ) )
213	211 212	eqtrd	⊢ ( Lim 𝑦 → if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) = ∪ ( 𝑓 “ 𝑦 ) )
214	213	eqeq2d	⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) )
215	214	biimprd	⊢ ( Lim 𝑦 → ( 𝑥 = ∪ ( 𝑓 “ 𝑦 ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
216	215	adantld	⊢ ( Lim 𝑦 → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
217	205 210 216	3syld	⊢ ( Lim 𝑦 → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
218	217	adantl	⊢ ( ( 𝑦 ∈ V ∧ Lim 𝑦 ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) → 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
219	214	biimpd	⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) )
220	219	anc2li	⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ) )
221		orc	⊢ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) )
222	221	olcd	⊢ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
223	220 222	syl6	⊢ ( Lim 𝑦 → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
224	223	adantl	⊢ ( ( 𝑦 ∈ V ∧ Lim 𝑦 ) → ( 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) → ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
225	218 224	impbid	⊢ ( ( 𝑦 ∈ V ∧ Lim 𝑦 ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
226	164 202 225	3jaoi	⊢ ( ( 𝑦 = ∅ ∨ ∃ 𝑧 ∈ On 𝑦 = suc 𝑧 ∨ ( 𝑦 ∈ V ∧ Lim 𝑦 ) ) → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
227	137 226	sylbi	⊢ ( 𝑦 ∈ On → ( ( ( 𝑦 = ∅ ∧ 𝑥 = ∪ { 𝐴 } ) ∨ ( ( Lim 𝑦 ∧ 𝑥 = ∪ ( 𝑓 “ 𝑦 ) ) ∨ ( ∃ 𝑧 𝑦 = suc 𝑧 ∧ 𝑥 = ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
228	136 227	bitrid	⊢ ( 𝑦 ∈ On → ( ⟨ 𝑓 , 𝑦 ⟩ ( ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) ∪ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) ) 𝑥 ↔ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
229	53 228	syl	⊢ ( ( 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	⊢ ( 𝑥 ^◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ ⟨ 𝑓 , 𝑦 ⟩ Apply 𝑥 )
231	12 39 26	brapply	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ Apply 𝑥 ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) )
232	230 231	bitri	⊢ ( 𝑥 ^◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) )
233	232	a1i	⊢ ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ∧ 𝑦 ∈ dom 𝑓 ) → ( 𝑥 ^◡ Apply ⟨ 𝑓 , 𝑦 ⟩ ↔ 𝑥 = ( 𝑓 ‘ 𝑦 ) ) )
234	229 233	anbi12d	⊢ ( ( 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	⊢ ( ( 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	⊢ ( ( 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	⊢ ( 𝑓 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	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ∈ 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	⊢ ( ⟨ 𝑓 , 𝑦 ⟩ ( ^◡ 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	⊢ ( 𝑓 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	⊢ ( 𝑓 ‘ 𝑦 ) ∈ V
242	241	eqvinc	⊢ ( ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∃ 𝑥 ( 𝑥 = ( 𝑓 ‘ 𝑦 ) ∧ 𝑥 = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
243	236 240 242	3bitr4g	⊢ ( ( 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	⊢ ( ( 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	⊢ ( ( 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	⊢ ( ( 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	⊢ ( ( 𝑦 ∈ dom 𝑓 ∧ ¬ ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ¬ ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
248	246 247	bitrdi	⊢ ( ( 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	⊢ ( ( 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	⊢ ( ( 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	⊢ ( ∃ 𝑦 ¬ ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ¬ ∀ 𝑦 ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
252	250 251	bitr2di	⊢ ( ( 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	⊢ ( 𝑓 ∈ 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	⊢ ( ( 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	⊢ ( ( 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	⊢ ( ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ dom 𝑓 → ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) )
257	255 256	bitr4di	⊢ ( ( 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	⊢ ( ( ( 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	⊢ ( ( ( Fun 𝑓 ∧ dom 𝑓 ∈ On ) ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ↔ ( Fun 𝑓 ∧ ( dom 𝑓 ∈ On ∧ ∀ 𝑦 ∈ dom 𝑓 ( 𝑓 ‘ 𝑦 ) = if ( 𝑦 = ∅ , if ( 𝐴 ∈ V , 𝐴 , ∅ ) , if ( Lim 𝑦 , ∪ ( 𝑓 “ 𝑦 ) , ( 𝐹 ‘ ( 𝑓 ‘ ∪ 𝑦 ) ) ) ) ) ) )
260	258 259	bitri	⊢ ( ( ( 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	⊢ ( 𝑓 ∈ ( ( 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	⊢ ( 𝑓 ∈ ( ( 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	⊢ ( ( 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	⊢ ∪ ( ( 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	⊢ rec ( 𝐹 , 𝐴 ) = ∪ ( ( Funs ∩ ( ^◡ Domain “ On ) ) ∖ dom ( ( ^◡ E ∘ Domain ) ∖ Fix ( ^◡ Apply ∘ ( ( ( V × { ∅ } ) × { ∪ { 𝐴 } } ) ∪ ( ( ( Bigcup ∘ Img ) ↾ ( V × Limits ) ) ∪ ( ( FullFun 𝐹 ∘ ( Apply ∘ pprod ( I , Bigcup ) ) ) ↾ ( V × ran Succ ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem dfrdg4

Proof