Metamath Proof Explorer

Theorem bnj1417

Description: Technical lemma for bnj60 . 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) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1417.1 ⊢ ( 𝜑 ↔ 𝑅 FrSe 𝐴 )
bnj1417.2 ⊢ ( 𝜓 ↔ ¬ 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
bnj1417.3 ⊢ ( 𝜒 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜓 ) )
bnj1417.4 ⊢ ( 𝜃 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒 ) )
bnj1417.5 ⊢ 𝐵 = ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
Assertion bnj1417 ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 bnj1417.1 ⊢ ( 𝜑 ↔ 𝑅 FrSe 𝐴 )
2 bnj1417.2 ⊢ ( 𝜓 ↔ ¬ 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
3 bnj1417.3 ⊢ ( 𝜒 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜓 ) )
4 bnj1417.4 ⊢ ( 𝜃 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒 ) )
5 bnj1417.5 ⊢ 𝐵 = ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∪ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
6 1 biimpi ⊢ ( 𝜑 → 𝑅 FrSe 𝐴 )
7 bnj1418 ⊢ ( 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑥 𝑅 𝑥 )
8 7 adantl ⊢ ( ( 𝜃 ∧ 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) → 𝑥 𝑅 𝑥 )
9 4 6 bnj835 ⊢ ( 𝜃 → 𝑅 FrSe 𝐴 )
10 df-bnj15 ⊢ ( 𝑅 FrSe 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) )
11 10 simplbi ⊢ ( 𝑅 FrSe 𝐴 → 𝑅 Fr 𝐴 )
12 9 11 syl ⊢ ( 𝜃 → 𝑅 Fr 𝐴 )
13 bnj213 ⊢ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝐴
14 13 sseli ⊢ ( 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑥 ∈ 𝐴 )
15 frirr ⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
16 12 14 15 syl2an ⊢ ( ( 𝜃 ∧ 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ¬ 𝑥 𝑅 𝑥 )
17 8 16 pm2.65da ⊢ ( 𝜃 → ¬ 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) )
18 nfv ⊢ Ⅎ 𝑦 𝜑
19 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
20 3 bnj1095 ⊢ ( 𝜒 → ∀ 𝑦 𝜒 )
21 20 nf5i ⊢ Ⅎ 𝑦 𝜒
22 18 19 21 nf3an ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒 )
23 4 22 nfxfr ⊢ Ⅎ 𝑦 𝜃
24 9 ad2antrr ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑅 FrSe 𝐴 )
25 simplr ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) )
26 13 25 sseldi ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ 𝐴 )
27 simpr ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
28 bnj1125 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → trCl ( 𝑥 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
29 24 26 27 28 syl3anc ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → trCl ( 𝑥 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
30 bnj1147 ⊢ trCl ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
31 30 27 sseldi ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑥 ∈ 𝐴 )
32 bnj906 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
33 24 31 32 syl2anc ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
34 33 25 sseldd ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
35 29 34 sseldd ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑦 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
36 3 biimpi ⊢ ( 𝜒 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜓 ) )
37 4 36 bnj837 ⊢ ( 𝜃 → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜓 ) )
38 37 ad2antrr ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜓 ) )
39 bnj1418 ⊢ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑦 𝑅 𝑥 )
40 39 ad2antlr ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → 𝑦 𝑅 𝑥 )
41 rsp ⊢ ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜓 ) → ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → [ 𝑦 / 𝑥 ] 𝜓 ) ) )
42 38 26 40 41 syl3c ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → [ 𝑦 / 𝑥 ] 𝜓 )
43 vex ⊢ 𝑦 ∈ V
44 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ↔ 𝑦 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ) )
45 bnj1318 ⊢ ( 𝑥 = 𝑦 → trCl ( 𝑥 , 𝐴 , 𝑅 ) = trCl ( 𝑦 , 𝐴 , 𝑅 ) )
46 45 eleq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑦 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ↔ 𝑦 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
47 44 46 bitrd ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ↔ 𝑦 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
48 47 notbid ⊢ ( 𝑥 = 𝑦 → ( ¬ 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ↔ ¬ 𝑦 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
49 2 48 syl5bb ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ ¬ 𝑦 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
50 43 49 sbcie ⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ ¬ 𝑦 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
51 42 50 sylib ⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ∧ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) → ¬ 𝑦 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
52 35 51 pm2.65da ⊢ ( ( 𝜃 ∧ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ) → ¬ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
53 52 ex ⊢ ( 𝜃 → ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → ¬ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
54 23 53 ralrimi ⊢ ( 𝜃 → ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ¬ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
55 ralnex ⊢ ( ∀ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ¬ 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) ↔ ¬ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
56 54 55 sylib ⊢ ( 𝜃 → ¬ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
57 eliun ⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ↔ ∃ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) 𝑥 ∈ trCl ( 𝑦 , 𝐴 , 𝑅 ) )
58 56 57 sylnibr ⊢ ( 𝜃 → ¬ 𝑥 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) )
59 ioran ⊢ ( ¬ ( 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∨ 𝑥 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( ¬ 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ ¬ 𝑥 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
60 17 58 59 sylanbrc ⊢ ( 𝜃 → ¬ ( 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∨ 𝑥 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
61 4 simp2bi ⊢ ( 𝜃 → 𝑥 ∈ 𝐴 )
62 5 bnj1414 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → trCl ( 𝑥 , 𝐴 , 𝑅 ) = 𝐵 )
63 9 61 62 syl2anc ⊢ ( 𝜃 → trCl ( 𝑥 , 𝐴 , 𝑅 ) = 𝐵 )
64 63 eleq2d ⊢ ( 𝜃 → ( 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ↔ 𝑥 ∈ 𝐵 ) )
65 5 bnj1138 ⊢ ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∨ 𝑥 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) )
66 64 65 bitrdi ⊢ ( 𝜃 → ( 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) ↔ ( 𝑥 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∨ 𝑥 ∈ ∪ 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) trCl ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
67 60 66 mtbird ⊢ ( 𝜃 → ¬ 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
68 67 2 sylibr ⊢ ( 𝜃 → 𝜓 )
69 4 68 sylbir ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝜒 ) → 𝜓 )
70 69 3exp ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜒 → 𝜓 ) ) )
71 70 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝜒 → 𝜓 ) )
72 3 bnj1204 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝜒 → 𝜓 ) ) → ∀ 𝑥 ∈ 𝐴 𝜓 )
73 6 71 72 syl2anc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 )
74 2 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )
75 73 74 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ trCl ( 𝑥 , 𝐴 , 𝑅 ) )