Metamath Proof Explorer

Theorem bnj978

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 bnj978.1 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
bnj978.2 ⊢ ( 𝜃 → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
Assertion bnj978 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 bnj978.1 ⊢ ( 𝜃 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2 bnj978.2 ⊢ ( 𝜃 → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
3 1 2 sylbir ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
4 3 gen2 ⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
5 bnj253 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6 5 imbi1i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
7 6 2albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
8 3impexp ⊢ ( ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
9 8 2albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
10 19.21v ⊢ ( ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑧 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
11 19.21v ⊢ ( ∀ 𝑧 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
12 11 imbi2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑧 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
13 10 12 bitri ⊢ ( ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
14 13 albii ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) ↔ ∀ 𝑦 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
15 19.21v ⊢ ( ∀ 𝑦 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) )
16 df-ral ⊢ ( ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
17 16 bicomi ⊢ ( ∀ 𝑦 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ↔ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
18 17 imbi2i ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
19 14 15 18 3bitri ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
20 7 9 19 3bitri ⊢ ( ∀ 𝑦 ∀ 𝑧 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∧ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
21 4 20 mpbi ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
22 df-ss ⊢ ( pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
23 22 ralbii ⊢ ( ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
24 21 23 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
25 df-bnj19 ⊢ ( TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) ↔ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
26 24 25 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) )