This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1253

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

Proof

Step Hyp Ref Expression
1 bnj1253.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1253.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1253.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1253.4 ⊢ 𝐷 = ( dom 𝑔 ∩ dom ℎ )
5 bnj1253.5 ⊢ 𝐸 = { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) }
6 bnj1253.6 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ) )
7 bnj1253.7 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀ 𝑦 ∈ 𝐸 ¬ 𝑦 𝑅 𝑥 ) )
8 6 bnj1254 ⊢ ( 𝜑 → ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) )
9 1 2 3 4 5 6 7 bnj1256 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 𝑔 Fn 𝑑 )
10 4 bnj1292 ⊢ 𝐷 ⊆ dom 𝑔
11 fndm ⊢ ( 𝑔 Fn 𝑑 → dom 𝑔 = 𝑑 )
12 10 11 sseqtrid ⊢ ( 𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑 )
13 fnssres ⊢ ( ( 𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑 ) → ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
14 12 13 mpdan ⊢ ( 𝑔 Fn 𝑑 → ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
15 9 14 bnj31 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
16 15 bnj1265 ⊢ ( 𝜑 → ( 𝑔 ↾ 𝐷 ) Fn 𝐷 )
17 1 2 3 4 5 6 7 bnj1259 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ℎ Fn 𝑑 )
18 4 bnj1293 ⊢ 𝐷 ⊆ dom ℎ
19 fndm ⊢ ( ℎ Fn 𝑑 → dom ℎ = 𝑑 )
20 18 19 sseqtrid ⊢ ( ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑 )
21 fnssres ⊢ ( ( ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑 ) → ( ℎ ↾ 𝐷 ) Fn 𝐷 )
22 20 21 mpdan ⊢ ( ℎ Fn 𝑑 → ( ℎ ↾ 𝐷 ) Fn 𝐷 )
23 17 22 bnj31 ⊢ ( 𝜑 → ∃ 𝑑 ∈ 𝐵 ( ℎ ↾ 𝐷 ) Fn 𝐷 )
24 23 bnj1265 ⊢ ( 𝜑 → ( ℎ ↾ 𝐷 ) Fn 𝐷 )
25 ssid ⊢ 𝐷 ⊆ 𝐷
26 fvreseq ⊢ ( ( ( ( 𝑔 ↾ 𝐷 ) Fn 𝐷 ∧ ( ℎ ↾ 𝐷 ) Fn 𝐷 ) ∧ 𝐷 ⊆ 𝐷 ) → ( ( ( 𝑔 ↾ 𝐷 ) ↾ 𝐷 ) = ( ( ℎ ↾ 𝐷 ) ↾ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐷 ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ) )
27 25 26 mpan2 ⊢ ( ( ( 𝑔 ↾ 𝐷 ) Fn 𝐷 ∧ ( ℎ ↾ 𝐷 ) Fn 𝐷 ) → ( ( ( 𝑔 ↾ 𝐷 ) ↾ 𝐷 ) = ( ( ℎ ↾ 𝐷 ) ↾ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐷 ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ) )
28 16 24 27 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑔 ↾ 𝐷 ) ↾ 𝐷 ) = ( ( ℎ ↾ 𝐷 ) ↾ 𝐷 ) ↔ ∀ 𝑥 ∈ 𝐷 ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ) )
29 residm ⊢ ( ( 𝑔 ↾ 𝐷 ) ↾ 𝐷 ) = ( 𝑔 ↾ 𝐷 )
30 residm ⊢ ( ( ℎ ↾ 𝐷 ) ↾ 𝐷 ) = ( ℎ ↾ 𝐷 )
31 29 30 eqeq12i ⊢ ( ( ( 𝑔 ↾ 𝐷 ) ↾ 𝐷 ) = ( ( ℎ ↾ 𝐷 ) ↾ 𝐷 ) ↔ ( 𝑔 ↾ 𝐷 ) = ( ℎ ↾ 𝐷 ) )
32 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐷 ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ) )
33 28 31 32 3bitr3g ⊢ ( 𝜑 → ( ( 𝑔 ↾ 𝐷 ) = ( ℎ ↾ 𝐷 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ) ) )
34 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) )
35 fvres ⊢ ( 𝑥 ∈ 𝐷 → ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
36 34 35 eqeq12d ⊢ ( 𝑥 ∈ 𝐷 → ( ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ↔ ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) )
37 36 pm5.74i ⊢ ( ( 𝑥 ∈ 𝐷 → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) )
38 37 albii ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( ( 𝑔 ↾ 𝐷 ) ‘ 𝑥 ) = ( ( ℎ ↾ 𝐷 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) )
39 33 38 bitrdi ⊢ ( 𝜑 → ( ( 𝑔 ↾ 𝐷 ) = ( ℎ ↾ 𝐷 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ) )
40 39 necon3abid ⊢ ( 𝜑 → ( ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ↔ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ) )
41 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐷 ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐷 ∧ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ) )
42 pm4.61 ⊢ ( ¬ ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ¬ ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) )
43 df-ne ⊢ ( ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ↔ ¬ ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) )
44 43 anbi2i ⊢ ( ( 𝑥 ∈ 𝐷 ∧ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ¬ ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) )
45 42 44 bitr4i ⊢ ( ¬ ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ) )
46 45 exbii ⊢ ( ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐷 ∧ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ) )
47 exnal ⊢ ( ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ↔ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) )
48 41 46 47 3bitr2ri ⊢ ( ¬ ∀ 𝑥 ( 𝑥 ∈ 𝐷 → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐷 ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) )
49 40 48 bitrdi ⊢ ( 𝜑 → ( ( 𝑔 ↾ 𝐷 ) ≠ ( ℎ ↾ 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐷 ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) ) )
50 8 49 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐷 ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) )
51 5 neeq1i ⊢ ( 𝐸 ≠ ∅ ↔ { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ≠ ∅ )
52 rabn0 ⊢ ( { 𝑥 ∈ 𝐷 ∣ ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐷 ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) )
53 51 52 bitri ⊢ ( 𝐸 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐷 ( 𝑔 ‘ 𝑥 ) ≠ ( ℎ ‘ 𝑥 ) )
54 50 53 sylibr ⊢ ( 𝜑 → 𝐸 ≠ ∅ )