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	sselid	⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ 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	sselid	⊢ ( ( ( 𝜃 ∧ 𝑦 ∈ 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	bitrid	⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ ¬ 𝑦 ∈ 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 ( 𝑥 , 𝐴 , 𝑅 ) )

Metamath Proof Explorer

Theorem bnj1417

Proof