Theorem bnj1296

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

Proof

Step	Hyp	Ref	Expression
1		bnj1296.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2		bnj1296.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3		bnj1296.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4		bnj1296.4	⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5		bnj1296.5	⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6		bnj1296.6	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7		bnj1296.7	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8		bnj1296.18	⊢ ( 𝜓 → ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) )
9		bnj1296.9	⊢ 𝑍 = ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
10		bnj1296.10	⊢ 𝐾 = { 𝑔 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) }
11		bnj1296.11	⊢ 𝑊 = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
12		bnj1296.12	⊢ 𝐿 = { ℎ ∣ ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) }
13	8	opeq2d	⊢ ( 𝜓 → ⟨ 𝑥 , ( 𝑔 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑥 , ( ℎ ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ )
14	13 9 11	3eqtr4g	⊢ ( 𝜓 → 𝑍 = 𝑊 )
15	14	fveq2d	⊢ ( 𝜓 → ( 𝐺 ‘ 𝑍 ) = ( 𝐺 ‘ 𝑊 ) )
16	10	bnj1436	⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
17		fndm	⊢ ( 𝑔 Fn 𝑑 → dom 𝑔 = 𝑑 )
18	17	anim1i	⊢ ( ( 𝑔 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) → ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
19	16 18	bnj31	⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
20		raleq	⊢ ( dom 𝑔 = 𝑑 → ( ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ↔ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
21	20	pm5.32i	⊢ ( ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) ↔ ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
22	21	rexbii	⊢ ( ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
23	19 22	sylibr	⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) )
24		simpr	⊢ ( ( dom 𝑔 = 𝑑 ∧ ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) ) → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
25	23 24	bnj31	⊢ ( 𝑔 ∈ 𝐾 → ∃ 𝑑 ∈ 𝐵 ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
26	25	bnj1265	⊢ ( 𝑔 ∈ 𝐾 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
27	2 3 9 10	bnj1234	⊢ 𝐶 = 𝐾
28	26 27	eleq2s	⊢ ( 𝑔 ∈ 𝐶 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
29	6 28	bnj770	⊢ ( 𝜑 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
30	7 29	bnj835	⊢ ( 𝜓 → ∀ 𝑥 ∈ dom 𝑔 ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
31	4	bnj1292	⊢ 𝐷 ⊆ dom 𝑔
32	5 7	bnj1212	⊢ ( 𝜓 → 𝑥 ∈ 𝐷 )
33	31 32	bnj1213	⊢ ( 𝜓 → 𝑥 ∈ dom 𝑔 )
34	30 33	bnj1294	⊢ ( 𝜓 → ( 𝑔 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑍 ) )
35	12	bnj1436	⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
36		fndm	⊢ ( ℎ Fn 𝑑 → dom ℎ = 𝑑 )
37	36	anim1i	⊢ ( ( ℎ Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) → ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
38	35 37	bnj31	⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
39		raleq	⊢ ( dom ℎ = 𝑑 → ( ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ↔ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
40	39	pm5.32i	⊢ ( ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) ↔ ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
41	40	rexbii	⊢ ( ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) ↔ ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
42	38 41	sylibr	⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) )
43		simpr	⊢ ( ( dom ℎ = 𝑑 ∧ ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) ) → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
44	42 43	bnj31	⊢ ( ℎ ∈ 𝐿 → ∃ 𝑑 ∈ 𝐵 ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
45	44	bnj1265	⊢ ( ℎ ∈ 𝐿 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
46	2 3 11 12	bnj1234	⊢ 𝐶 = 𝐿
47	45 46	eleq2s	⊢ ( ℎ ∈ 𝐶 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
48	6 47	bnj771	⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
49	7 48	bnj835	⊢ ( 𝜓 → ∀ 𝑥 ∈ dom ℎ ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
50	4	bnj1293	⊢ 𝐷 ⊆ dom ℎ
51	50 32	bnj1213	⊢ ( 𝜓 → 𝑥 ∈ dom ℎ )
52	49 51	bnj1294	⊢ ( 𝜓 → ( ℎ ‘ 𝑥 ) = ( 𝐺 ‘ 𝑊 ) )
53	15 34 52	3eqtr4d	⊢ ( 𝜓 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )