Theorem bnj1279

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) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj1279.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
	bnj1279.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
	bnj1279.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
	bnj1279.4	⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
	bnj1279.5	⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
	bnj1279.6	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
	bnj1279.7	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
Assertion	bnj1279	⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		bnj1279.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2		bnj1279.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3		bnj1279.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4		bnj1279.4	⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5		bnj1279.5	⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6		bnj1279.6	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7		bnj1279.7	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8		n0	⊢ ( ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) )
9		elin	⊢ ( 𝑦 ∈ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ↔ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) )
10	9	exbii	⊢ ( ∃ 𝑦 𝑦 ∈ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ↔ ∃ 𝑦 ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) )
11	8 10	sylbb	⊢ ( ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ → ∃ 𝑦 ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) )
12		df-bnj14	⊢ pred ( 𝑥 , 𝐴 , 𝑅 ) = { 𝑦 ∈ 𝐴 ∣ 𝑦 𝑅 𝑥 }
13	12	bnj1538	⊢ ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) → 𝑦 𝑅 𝑥 )
14	13	anim1i	⊢ ( ( 𝑦 ∈ pred ( 𝑥 , 𝐴 , 𝑅 ) ∧ 𝑦 ∈ 𝐸 ) → ( 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
15	11 14	bnj593	⊢ ( ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ → ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
16	15	3ad2ant3	⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) → ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
17		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐸
18		nfra1	⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥
19		nfv	⊢ Ⅎ 𝑦 ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅
20	17 18 19	nf3an	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ )
21	20	nf5ri	⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) → ∀ 𝑦 ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) )
22	16 21	bnj1275	⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) → ∃ 𝑦 ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) )
23		simp2	⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → 𝑦 𝑅 𝑥 )
24		simp12	⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 )
25		simp3	⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → 𝑦 ∈ 𝐸 )
26	24 25	bnj1294	⊢ ( ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ) ∧ 𝑦 𝑅 𝑥 ∧ 𝑦 ∈ 𝐸 ) → ¬ 𝑦 𝑅 𝑥 )
27	22 23 26	bnj1304	⊢ ¬ ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ∧ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ )
28	27	bnj1224	⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) → ¬ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ )
29		nne	⊢ ( ¬ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) ≠ ∅ ↔ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ )
30	28 29	sylib	⊢ ( ( 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∩ 𝐸 ) = ∅ )