bnj907

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	bnj907.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj907.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj907.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj907.4	⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj907.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
	bnj907.6	⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
	bnj907.7	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
	bnj907.8	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
	bnj907.9	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
	bnj907.10	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
	bnj907.11	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
	bnj907.12	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
	bnj907.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj907.14	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
	bnj907.15	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj907.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
Assertion	bnj907	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj907.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj907.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj907.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4		bnj907.4	⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5		bnj907.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
6		bnj907.6	⊢ ( 𝜂 ↔ ( 𝑖 ∈ 𝑛 ∧ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) ) )
7		bnj907.7	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
8		bnj907.8	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
9		bnj907.9	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
10		bnj907.10	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
11		bnj907.11	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
12		bnj907.12	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
13		bnj907.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
14		bnj907.14	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
15		bnj907.15	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
16		bnj907.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
17	1 2 3 4 5 6 13 14	bnj1021	⊢ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) )
18		vex	⊢ 𝑝 ∈ V
19	3 7 8 9 18	bnj919	⊢ ( 𝜒′ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝑓 Fn 𝑝 ∧ 𝜑′ ∧ 𝜓′ ) )
20	16	bnj918	⊢ 𝐺 ∈ V
21	19 10 11 12 20	bnj976	⊢ ( 𝜒″ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) )
22	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 21	bnj1020	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
23	22	ax-gen	⊢ ∀ 𝑚 ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
24		19.29r	⊢ ( ( ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ∀ 𝑚 ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑚 ( ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
25		pm3.33	⊢ ( ( ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) → ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
26	24 25	bnj593	⊢ ( ( ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) ∧ ∀ 𝑚 ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) → ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
27	23 26	mpan2	⊢ ( ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) → ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
28	27	2eximi	⊢ ( ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ) → ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
29	17 28	bnj101	⊢ ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
30		19.9v	⊢ ( ∃ 𝑓 ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
31	29 30	mpbi	⊢ ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
32		19.9v	⊢ ( ∃ 𝑛 ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
33	31 32	mpbi	⊢ ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
34		19.9v	⊢ ( ∃ 𝑖 ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
35	33 34	mpbi	⊢ ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
36		19.9v	⊢ ( ∃ 𝑚 ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
37	35 36	mpbi	⊢ ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
38	4	bnj1254	⊢ ( 𝜃 → 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) )
39	37 38	sseldd	⊢ ( 𝜃 → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
40	4 39	bnj978	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) )

Metamath Proof Explorer

Theorem bnj907

Proof