bnj983

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj983.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj983.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj983.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj983.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
	bnj983.5	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
Assertion	bnj983	⊢ ( 𝑍 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bnj983.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj983.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj983.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj983.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5		bnj983.5	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
6	1 2 3 4	bnj882	⊢ trCl ( 𝑋 , 𝐴 , 𝑅 ) = ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 )
7	6	eleq2i	⊢ ( 𝑍 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ 𝑍 ∈ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) )
8		eliun	⊢ ( 𝑍 ∈ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ∈ 𝐵 𝑍 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) )
9		eliun	⊢ ( 𝑍 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) )
10	9	rexbii	⊢ ( ∃ 𝑓 ∈ 𝐵 𝑍 ∈ ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ∈ 𝐵 ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) )
11	8 10	bitri	⊢ ( 𝑍 ∈ ∪ 𝑓 ∈ 𝐵 ∪ 𝑖 ∈ dom 𝑓 ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ∈ 𝐵 ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) )
12		df-rex	⊢ ( ∃ 𝑓 ∈ 𝐵 ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ( 𝑓 ∈ 𝐵 ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
13	4	eqabri	⊢ ( 𝑓 ∈ 𝐵 ↔ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
14	13	anbi1i	⊢ ( ( 𝑓 ∈ 𝐵 ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
15	14	exbii	⊢ ( ∃ 𝑓 ( 𝑓 ∈ 𝐵 ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ∃ 𝑓 ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
16	12 15	bitri	⊢ ( ∃ 𝑓 ∈ 𝐵 ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑓 ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
17	7 11 16	3bitri	⊢ ( 𝑍 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
18		bnj252	⊢ ( ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
19	5 18	bitri	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
20	19	exbii	⊢ ( ∃ 𝑛 𝜒 ↔ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
21	20	anbi1i	⊢ ( ( ∃ 𝑛 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
22		df-rex	⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) )
23		df-rex	⊢ ( ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ↔ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
24	22 23	anbi12i	⊢ ( ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
25	21 24	bitr4i	⊢ ( ( ∃ 𝑛 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ ∃ 𝑖 ∈ dom 𝑓 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
26	17 25	bnj133	⊢ ( 𝑍 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ( ∃ 𝑛 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
27		19.41v	⊢ ( ∃ 𝑛 ( 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( ∃ 𝑛 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
28	26 27	bnj133	⊢ ( 𝑍 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ∃ 𝑛 ( 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
29	2	bnj1095	⊢ ( 𝜓 → ∀ 𝑖 𝜓 )
30	29 5	bnj1096	⊢ ( 𝜒 → ∀ 𝑖 𝜒 )
31	30	nf5i	⊢ Ⅎ 𝑖 𝜒
32	31	19.42	⊢ ( ∃ 𝑖 ( 𝜒 ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ( 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
33	32	2exbii	⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑓 ∃ 𝑛 ( 𝜒 ∧ ∃ 𝑖 ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
34	28 33	bitr4i	⊢ ( 𝑍 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
35		3anass	⊢ ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝜒 ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
36	35	3exbii	⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ ( 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
37		fndm	⊢ ( 𝑓 Fn 𝑛 → dom 𝑓 = 𝑛 )
38	5 37	bnj770	⊢ ( 𝜒 → dom 𝑓 = 𝑛 )
39		eleq2	⊢ ( dom 𝑓 = 𝑛 → ( 𝑖 ∈ dom 𝑓 ↔ 𝑖 ∈ 𝑛 ) )
40	39	3anbi2d	⊢ ( dom 𝑓 = 𝑛 → ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
41	38 40	syl	⊢ ( 𝜒 → ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
42	41	3ad2ant1	⊢ ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) → ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
43	42	ibi	⊢ ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) → ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
44	41	3ad2ant1	⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) → ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ) )
45	44	ibir	⊢ ( ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) → ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
46	43 45	impbii	⊢ ( ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
47	46	3exbii	⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ dom 𝑓 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )
48	34 36 47	3bitr2i	⊢ ( 𝑍 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ( 𝜒 ∧ 𝑖 ∈ 𝑛 ∧ 𝑍 ∈ ( 𝑓 ‘ 𝑖 ) ) )

Metamath Proof Explorer

Theorem bnj983

Proof