Metamath Proof Explorer


Theorem 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 ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) )