bnj1286

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

Proof

Step	Hyp	Ref	Expression
1		bnj1286.1	⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2		bnj1286.2	⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3		bnj1286.3	⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4		bnj1286.4	⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5		bnj1286.5	⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6		bnj1286.6	⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7		bnj1286.7	⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8	1 2 3 4 5 6 7	bnj1256	⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 𝑔 Fn 𝑑 )
9	8	bnj1196	⊢ ( 𝜑 → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ 𝑔 Fn 𝑑 ) )
10	1	bnj1517	⊢ ( 𝑑 ∈ 𝐵 → ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
11	10	adantr	⊢ ( ( 𝑑 ∈ 𝐵 ∧ 𝑔 Fn 𝑑 ) → ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
12		fndm	⊢ ( 𝑔 Fn 𝑑 → dom 𝑔 = 𝑑 )
13		sseq2	⊢ ( dom 𝑔 = 𝑑 → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 ↔ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
14	13	raleqbi1dv	⊢ ( dom 𝑔 = 𝑑 → ( ∀ 𝑥 ∈ dom 𝑔 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 ↔ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
15	12 14	syl	⊢ ( 𝑔 Fn 𝑑 → ( ∀ 𝑥 ∈ dom 𝑔 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 ↔ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
16	15	adantl	⊢ ( ( 𝑑 ∈ 𝐵 ∧ 𝑔 Fn 𝑑 ) → ( ∀ 𝑥 ∈ dom 𝑔 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 ↔ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
17	11 16	mpbird	⊢ ( ( 𝑑 ∈ 𝐵 ∧ 𝑔 Fn 𝑑 ) → ∀ 𝑥 ∈ dom 𝑔 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 )
18	9 17	bnj593	⊢ ( 𝜑 → ∃ 𝑑 ∀ 𝑥 ∈ dom 𝑔 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 )
19	18	bnj937	⊢ ( 𝜑 → ∀ 𝑥 ∈ dom 𝑔 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 )
20	7 19	bnj835	⊢ ( 𝜓 → ∀ 𝑥 ∈ dom 𝑔 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 )
21	5	ssrab3	⊢ 𝐸 ⊆ 𝐷
22	4	bnj1292	⊢ 𝐷 ⊆ dom 𝑔
23	21 22	sstri	⊢ 𝐸 ⊆ dom 𝑔
24	23	sseli	⊢ ( 𝑥 ∈ 𝐸 → 𝑥 ∈ dom 𝑔 )
25	7 24	bnj836	⊢ ( 𝜓 → 𝑥 ∈ dom 𝑔 )
26	20 25	bnj1294	⊢ ( 𝜓 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom 𝑔 )
27	1 2 3 4 5 6 7	bnj1259	⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ℎ Fn 𝑑 )
28	27	bnj1196	⊢ ( 𝜑 → ∃ 𝑑 ( 𝑑 ∈ 𝐵 ∧ ℎ Fn 𝑑 ) )
29	10	adantr	⊢ ( ( 𝑑 ∈ 𝐵 ∧ ℎ Fn 𝑑 ) → ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 )
30		fndm	⊢ ( ℎ Fn 𝑑 → dom ℎ = 𝑑 )
31		sseq2	⊢ ( dom ℎ = 𝑑 → ( pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ ↔ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
32	31	raleqbi1dv	⊢ ( dom ℎ = 𝑑 → ( ∀ 𝑥 ∈ dom ℎ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ ↔ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
33	30 32	syl	⊢ ( ℎ Fn 𝑑 → ( ∀ 𝑥 ∈ dom ℎ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ ↔ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
34	33	adantl	⊢ ( ( 𝑑 ∈ 𝐵 ∧ ℎ Fn 𝑑 ) → ( ∀ 𝑥 ∈ dom ℎ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ ↔ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) )
35	29 34	mpbird	⊢ ( ( 𝑑 ∈ 𝐵 ∧ ℎ Fn 𝑑 ) → ∀ 𝑥 ∈ dom ℎ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ )
36	28 35	bnj593	⊢ ( 𝜑 → ∃ 𝑑 ∀ 𝑥 ∈ dom ℎ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ )
37	36	bnj937	⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ℎ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ )
38	7 37	bnj835	⊢ ( 𝜓 → ∀ 𝑥 ∈ dom ℎ pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ )
39	4	bnj1293	⊢ 𝐷 ⊆ dom ℎ
40	21 39	sstri	⊢ 𝐸 ⊆ dom ℎ
41	40	sseli	⊢ ( 𝑥 ∈ 𝐸 → 𝑥 ∈ dom ℎ )
42	7 41	bnj836	⊢ ( 𝜓 → 𝑥 ∈ dom ℎ )
43	38 42	bnj1294	⊢ ( 𝜓 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ dom ℎ )
44	26 43	ssind	⊢ ( 𝜓 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ ( dom 𝑔 ∩ dom ℎ ) )
45	44 4	sseqtrrdi	⊢ ( 𝜓 → pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝐷 )

Metamath Proof Explorer

Theorem bnj1286

Proof