Theorem bnj1018g

Description: Version of bnj1018 with less disjoint variable conditions, but requiring ax-13 . (Contributed by GG, 27-Mar-2024) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1018.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj1018.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj1018.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj1018.4	⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj1018.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
	bnj1018.7	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
	bnj1018.8	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
	bnj1018.9	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
	bnj1018.10	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
	bnj1018.11	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
	bnj1018.12	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
	bnj1018.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj1018.14	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
	bnj1018.15	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
	bnj1018.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
	bnj1018.26	⊢ ( 𝜒″ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) )
	bnj1018.29	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝜒″ )
	bnj1018.30	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) )
Assertion	bnj1018g	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → ( 𝐺 ‘ suc 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1018.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj1018.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj1018.3	⊢ ( 𝜒 ↔ ( 𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
4		bnj1018.4	⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5		bnj1018.5	⊢ ( 𝜏 ↔ ( 𝑚 ∈ ω ∧ 𝑛 = suc 𝑚 ∧ 𝑝 = suc 𝑛 ) )
6		bnj1018.7	⊢ ( 𝜑′ ↔ [ 𝑝 / 𝑛 ] 𝜑 )
7		bnj1018.8	⊢ ( 𝜓′ ↔ [ 𝑝 / 𝑛 ] 𝜓 )
8		bnj1018.9	⊢ ( 𝜒′ ↔ [ 𝑝 / 𝑛 ] 𝜒 )
9		bnj1018.10	⊢ ( 𝜑″ ↔ [ 𝐺 / 𝑓 ] 𝜑′ )
10		bnj1018.11	⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓′ )
11		bnj1018.12	⊢ ( 𝜒″ ↔ [ 𝐺 / 𝑓 ] 𝜒′ )
12		bnj1018.13	⊢ 𝐷 = ( ω ∖ { ∅ } )
13		bnj1018.14	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
14		bnj1018.15	⊢ 𝐶 = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑚 ) pred ( 𝑦 , 𝐴 , 𝑅 )
15		bnj1018.16	⊢ 𝐺 = ( 𝑓 ∪ { ⟨ 𝑛 , 𝐶 ⟩ } )
16		bnj1018.26	⊢ ( 𝜒″ ↔ ( 𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″ ) )
17		bnj1018.29	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → 𝜒″ )
18		bnj1018.30	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → ( 𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ) )
19		df-bnj17	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) ↔ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ) ∧ ∃ 𝑝 𝜏 ) )
20		bnj258	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ↔ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ) ∧ 𝜏 ) )
21	20 17	sylbir	⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ) ∧ 𝜏 ) → 𝜒″ )
22	21	ex	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ) → ( 𝜏 → 𝜒″ ) )
23	22	eximdv	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ) → ( ∃ 𝑝 𝜏 → ∃ 𝑝 𝜒″ ) )
24	3 8 11 13 15	bnj985	⊢ ( 𝐺 ∈ 𝐵 ↔ ∃ 𝑝 𝜒″ )
25	23 24	imbitrrdi	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ) → ( ∃ 𝑝 𝜏 → 𝐺 ∈ 𝐵 ) )
26	25	imp	⊢ ( ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ) ∧ ∃ 𝑝 𝜏 ) → 𝐺 ∈ 𝐵 )
27	19 26	sylbi	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → 𝐺 ∈ 𝐵 )
28		bnj1019	⊢ ( ∃ 𝑝 ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) ↔ ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) )
29	18	simp3d	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → suc 𝑖 ∈ 𝑝 )
30	16	bnj1235	⊢ ( 𝜒″ → 𝐺 Fn 𝑝 )
31		fndm	⊢ ( 𝐺 Fn 𝑝 → dom 𝐺 = 𝑝 )
32	17 30 31	3syl	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → dom 𝐺 = 𝑝 )
33	29 32	eleqtrrd	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → suc 𝑖 ∈ dom 𝐺 )
34	33	exlimiv	⊢ ( ∃ 𝑝 ( 𝜃 ∧ 𝜒 ∧ 𝜏 ∧ 𝜂 ) → suc 𝑖 ∈ dom 𝐺 )
35	28 34	sylbir	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → suc 𝑖 ∈ dom 𝐺 )
36	15	bnj918	⊢ 𝐺 ∈ V
37		vex	⊢ 𝑖 ∈ V
38	37	sucex	⊢ suc 𝑖 ∈ V
39	1 2 12 13 36 38	bnj1015	⊢ ( ( 𝐺 ∈ 𝐵 ∧ suc 𝑖 ∈ dom 𝐺 ) → ( 𝐺 ‘ suc 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
40	27 35 39	syl2anc	⊢ ( ( 𝜃 ∧ 𝜒 ∧ 𝜂 ∧ ∃ 𝑝 𝜏 ) → ( 𝐺 ‘ suc 𝑖 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )