Theorem bnj1245

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	bnj1245.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
	bnj1245.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
	bnj1245.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
	bnj1245.4	⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
	bnj1245.5	⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
	bnj1245.6	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
	bnj1245.7	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
	bnj1245.8	⊢ 𝑍 = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
	bnj1245.9	⊢ 𝐾 = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) }
Assertion	bnj1245	⊢ ( 𝜑 → dom ℎ ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bnj1245.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2		bnj1245.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3		bnj1245.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4		bnj1245.4	⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5		bnj1245.5	⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6		bnj1245.6	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7		bnj1245.7	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8		bnj1245.8	⊢ 𝑍 = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
9		bnj1245.9	⊢ 𝐾 = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) }
10	6	bnj1247	⊢ ( 𝜑 → ℎ ∈ 𝐶 )
11	2 3 8 9	bnj1234	⊢ 𝐶 = 𝐾
12	10 11	eleqtrdi	⊢ ( 𝜑 → ℎ ∈ 𝐾 )
13	9	abeq2i	⊢ ( ℎ ∈ 𝐾 ↔ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
14	13	bnj1238	⊢ ( ℎ ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ℎ Fn 𝑑 )
15	14	bnj1196	⊢ ( ℎ ∈ 𝐾 → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ ℎ Fn 𝑑 ) )
16	1	abeq2i	⊢ ( 𝑑 ∈ 𝐵 ↔ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
17	16	simplbi	⊢ ( 𝑑 ∈ 𝐵 → 𝑑 ⊆ 𝐴 )
18		fndm	⊢ ( ℎ Fn 𝑑 → dom ℎ = 𝑑 )
19	17 18	bnj1241	⊢ ( ( 𝑑 ∈ 𝐵 ∧ ℎ Fn 𝑑 ) → dom ℎ ⊆ 𝐴 )
20	15 19	bnj593	⊢ ( ℎ ∈ 𝐾 → ∃ 𝑑 dom ℎ ⊆ 𝐴 )
21	20	bnj937	⊢ ( ℎ ∈ 𝐾 → dom ℎ ⊆ 𝐴 )
22	12 21	syl	⊢ ( 𝜑 → dom ℎ ⊆ 𝐴 )