This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1137

Description: Property of _trCl . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1137.1 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
Assertion bnj1137 ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( 𝐵 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 bnj1137.1 ⊢ 𝐵 = ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
2 1 eleq2i ⊢ ( 𝑣 ∈ 𝐵 ↔ 𝑣 ∈ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
3 elun ⊢ ( 𝑣 ∈ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∨ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
4 2 3 bitri ⊢ ( 𝑣 ∈ 𝐵 ↔ ( 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∨ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
5 bnj213 ⊢ pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ 𝐴
6 5 sseli ⊢ ( 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) → 𝑣 ∈ 𝐴 )
7 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑣 ∈ 𝐴 ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑣 , 𝐴 , 𝑅 ) )
8 7 adantlr ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐴 ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑣 , 𝐴 , 𝑅 ) )
9 6 8 sylan2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑣 , 𝐴 , 𝑅 ) )
10 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → pred ( 𝑋 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
11 10 sselda ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → 𝑣 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
12 bnj18eq1 ⊢ ( 𝑦 = 𝑣 → trCl ( 𝑦 , 𝐴 , 𝑅 ) = trCl ( 𝑣 , 𝐴 , 𝑅 ) )
13 12 ssiun2s ⊢ ( 𝑣 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑣 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
14 11 13 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑣 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
15 9 14 sstrd ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
16 bnj1147 ⊢ trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
17 16 rgenw ⊢ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
18 iunss ⊢ ( ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴 ↔ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴 )
19 17 18 mpbir ⊢ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
20 19 sseli ⊢ ( 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) → 𝑣 ∈ 𝐴 )
21 20 8 sylan2 ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑣 , 𝐴 , 𝑅 ) )
22 bnj1125 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
23 22 3expia ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) → trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ) )
24 23 ralrimiv ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
25 iunss ⊢ ( ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) ↔ ∀ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
26 24 25 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
27 26 sselda ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑣 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) )
28 27 13 syl ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → trCl ( 𝑣 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
29 21 28 sstrd ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
30 15 29 jaodan ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∨ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
31 ssun2 ⊢ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ ( pred ( 𝑋 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
32 31 1 sseqtrri ⊢ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐵
33 30 32 sstrdi ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝑣 ∈ pred ( 𝑋 , 𝐴 , 𝑅 ) ∨ 𝑣 ∈ ∪ 𝑦 ∈ trCl ( 𝑋 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
34 4 33 sylan2b ⊢ ( ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝐵 ) → pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
35 34 ralrimiva ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑣 ∈ 𝐵 pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
36 df-bnj19 ⊢ ( TrFo ( 𝐵 , 𝐴 , 𝑅 ) ↔ ∀ 𝑣 ∈ 𝐵 pred ( 𝑣 , 𝐴 , 𝑅 ) ⊆ 𝐵 )
37 35 36 sylibr ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → TrFo ( 𝐵 , 𝐴 , 𝑅 ) )