Metamath Proof Explorer

Theorem bnj1125

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj1125 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
2 bnj1127 ⊢ ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → 𝑌 ∈ 𝐴 )
3 2 3ad2ant3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑌 ∈ 𝐴 )
4 bnj893 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
5 4 3adant3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V )
6 bnj1029 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) )
7 6 3adant3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) )
8 simp3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
9 elisset ⊢ ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ∃ 𝑦 𝑦 = 𝑌 )
10 9 3ad2ant3 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → ∃ 𝑦 𝑦 = 𝑌 )
11 df-bnj19 ⊢ ( TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) ↔ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
12 rsp ⊢ ( ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
13 11 12 sylbi ⊢ ( TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
14 7 13 syl ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
15 eleq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
16 bnj602 ⊢ ( 𝑦 = 𝑌 → pred ( 𝑦 , 𝐴 , 𝑅 ) = pred ( 𝑌 , 𝐴 , 𝑅 ) )
17 16 sseq1d ⊢ ( 𝑦 = 𝑌 → ( pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
18 15 17 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
19 14 18 syl5ib ⊢ ( 𝑦 = 𝑌 → ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
20 19 exlimiv ⊢ ( ∃ 𝑦 𝑦 = 𝑌 → ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) )
21 10 20 mpcom ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → ( 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
22 8 21 mpd ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
23 biid ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑌 ∈ 𝐴 ) ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑌 ∈ 𝐴 ) )
24 biid ⊢ ( ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ∧ TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) ∧ pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ↔ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ∧ TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) ∧ pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
25 23 24 bnj1124 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑌 ∈ 𝐴 ) ∧ ( trCl ( 𝑋 , 𝐴 , 𝑅 ) ∈ V ∧ TrFo ( trCl ( 𝑋 , 𝐴 , 𝑅 ) , 𝐴 , 𝑅 ) ∧ pred ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) ) → trCl ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
26 1 3 5 7 22 25 syl23anc ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑌 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )