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