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

Metamath Proof Explorer

Theorem bnj1523

Description: Technical lemma for bnj1522 . 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 bnj1523.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
bnj1523.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
bnj1523.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
bnj1523.4 ⊢ 𝐹 = ∪ 𝐶
bnj1523.5 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
bnj1523.6 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) )
bnj1523.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ) )
bnj1523.8 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) }
bnj1523.9 ⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑦 ∈ 𝐷 ∧ ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 ) )
Assertion bnj1523 ( ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) → 𝐹 = 𝐻 )

Proof

Step Hyp Ref Expression
1 bnj1523.1 ⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) }
2 bnj1523.2 ⊢ 𝑌 = ⟨ 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩
3 bnj1523.3 ⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) }
4 bnj1523.4 ⊢ 𝐹 = ∪ 𝐶
5 bnj1523.5 ⊢ ( 𝜑 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) )
6 bnj1523.6 ⊢ ( 𝜓 ↔ ( 𝜑 ∧ 𝐹 ≠ 𝐻 ) )
7 bnj1523.7 ⊢ ( 𝜒 ↔ ( 𝜓 ∧ 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ) )
8 bnj1523.8 ⊢ 𝐷 = { 𝑥 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) }
9 bnj1523.9 ⊢ ( 𝜃 ↔ ( 𝜒 ∧ 𝑦 ∈ 𝐷 ∧ ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 ) )
10 1 2 3 4 bnj60 ⊢ ( 𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴 )
11 5 10 bnj835 ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
12 6 11 bnj832 ⊢ ( 𝜓 → 𝐹 Fn 𝐴 )
13 7 12 bnj835 ⊢ ( 𝜒 → 𝐹 Fn 𝐴 )
14 9 13 bnj835 ⊢ ( 𝜃 → 𝐹 Fn 𝐴 )
15 5 simp2bi ⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
16 6 15 bnj832 ⊢ ( 𝜓 → 𝐻 Fn 𝐴 )
17 7 16 bnj835 ⊢ ( 𝜒 → 𝐻 Fn 𝐴 )
18 9 17 bnj835 ⊢ ( 𝜃 → 𝐻 Fn 𝐴 )
19 bnj213 ⊢ pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴
20 19 a1i ⊢ ( 𝜃 → pred ( 𝑦 , 𝐴 , 𝑅 ) ⊆ 𝐴 )
21 9 simp3bi ⊢ ( 𝜃 → ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 )
22 21 bnj1211 ⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 ∈ 𝐷 → ¬ 𝑧 𝑅 𝑦 ) )
23 con2b ⊢ ( ( 𝑧 ∈ 𝐷 → ¬ 𝑧 𝑅 𝑦 ) ↔ ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) )
24 23 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝐷 → ¬ 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) )
25 22 24 sylib ⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) )
26 bnj1418 ⊢ ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → 𝑧 𝑅 𝑦 )
27 26 imim1i ⊢ ( ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) → ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐷 ) )
28 27 alimi ⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑦 → ¬ 𝑧 ∈ 𝐷 ) → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐷 ) )
29 25 28 syl ⊢ ( 𝜃 → ∀ 𝑧 ( 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) → ¬ 𝑧 ∈ 𝐷 ) )
30 29 bnj1142 ⊢ ( 𝜃 → ∀ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ¬ 𝑧 ∈ 𝐷 )
31 1 bnj1309 ⊢ ( 𝑤 ∈ 𝐵 → ∀ 𝑥 𝑤 ∈ 𝐵 )
32 3 31 bnj1307 ⊢ ( 𝑤 ∈ 𝐶 → ∀ 𝑥 𝑤 ∈ 𝐶 )
33 32 nfcii ⊢ Ⅎ 𝑥 𝐶
34 33 nfuni ⊢ Ⅎ 𝑥 ∪ 𝐶
35 4 34 nfcxfr ⊢ Ⅎ 𝑥 𝐹
36 35 nfcrii ⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 )
37 8 36 bnj1534 ⊢ 𝐷 = { 𝑧 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐻 ‘ 𝑧 ) }
38 30 19 37 bnj1533 ⊢ ( 𝜃 → ∀ 𝑧 ∈ pred ( 𝑦 , 𝐴 , 𝑅 ) ( 𝐹 ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) )
39 14 18 20 38 bnj1536 ⊢ ( 𝜃 → ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) = ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
40 39 opeq2d ⊢ ( 𝜃 → ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ = ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ )
41 40 fveq2d ⊢ ( 𝜃 → ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
42 1 2 3 4 bnj1500 ⊢ ( 𝑅 FrSe 𝐴 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
43 5 42 bnj835 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
44 6 43 bnj832 ⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
45 7 44 bnj835 ⊢ ( 𝜒 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
46 45 36 bnj1529 ⊢ ( 𝜒 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
47 9 46 bnj835 ⊢ ( 𝜃 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
48 8 ssrab3 ⊢ 𝐷 ⊆ 𝐴
49 9 simp2bi ⊢ ( 𝜃 → 𝑦 ∈ 𝐷 )
50 48 49 bnj1213 ⊢ ( 𝜃 → 𝑦 ∈ 𝐴 )
51 47 50 bnj1294 ⊢ ( 𝜃 → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
52 5 simp3bi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
53 6 52 bnj832 ⊢ ( 𝜓 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
54 7 53 bnj835 ⊢ ( 𝜒 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) )
55 ax-5 ⊢ ( 𝑣 ∈ 𝐻 → ∀ 𝑥 𝑣 ∈ 𝐻 )
56 54 55 bnj1529 ⊢ ( 𝜒 → ∀ 𝑦 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
57 9 56 bnj835 ⊢ ( 𝜃 → ∀ 𝑦 ∈ 𝐴 ( 𝐻 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
58 57 50 bnj1294 ⊢ ( 𝜃 → ( 𝐻 ‘ 𝑦 ) = ( 𝐺 ‘ ⟨ 𝑦 , ( 𝐻 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ⟩ ) )
59 41 51 58 3eqtr4d ⊢ ( 𝜃 → ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
60 8 36 bnj1534 ⊢ 𝐷 = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐻 ‘ 𝑦 ) }
61 60 bnj1538 ⊢ ( 𝑦 ∈ 𝐷 → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐻 ‘ 𝑦 ) )
62 9 61 bnj836 ⊢ ( 𝜃 → ( 𝐹 ‘ 𝑦 ) ≠ ( 𝐻 ‘ 𝑦 ) )
63 62 neneqd ⊢ ( 𝜃 → ¬ ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) )
64 59 63 pm2.65i ⊢ ¬ 𝜃
65 64 nex ⊢ ¬ ∃ 𝑦 𝜃
66 5 simp1bi ⊢ ( 𝜑 → 𝑅 FrSe 𝐴 )
67 6 66 bnj832 ⊢ ( 𝜓 → 𝑅 FrSe 𝐴 )
68 7 67 bnj835 ⊢ ( 𝜒 → 𝑅 FrSe 𝐴 )
69 48 a1i ⊢ ( 𝜒 → 𝐷 ⊆ 𝐴 )
70 7 simp2bi ⊢ ( 𝜒 → 𝑥 ∈ 𝐴 )
71 7 simp3bi ⊢ ( 𝜒 → ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) )
72 8 reqabi ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) ) )
73 70 71 72 sylanbrc ⊢ ( 𝜒 → 𝑥 ∈ 𝐷 )
74 73 ne0d ⊢ ( 𝜒 → 𝐷 ≠ ∅ )
75 bnj69 ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝐷 ≠ ∅ ) → ∃ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 )
76 68 69 74 75 syl3anc ⊢ ( 𝜒 → ∃ 𝑦 ∈ 𝐷 ∀ 𝑧 ∈ 𝐷 ¬ 𝑧 𝑅 𝑦 )
77 76 9 bnj1209 ⊢ ( 𝜒 → ∃ 𝑦 𝜃 )
78 65 77 mto ⊢ ¬ 𝜒
79 78 nex ⊢ ¬ ∃ 𝑥 𝜒
80 6 simprbi ⊢ ( 𝜓 → 𝐹 ≠ 𝐻 )
81 12 16 80 36 bnj1542 ⊢ ( 𝜓 → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≠ ( 𝐻 ‘ 𝑥 ) )
82 1 2 3 4 5 6 bnj1525 ⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
83 81 7 82 bnj1521 ⊢ ( 𝜓 → ∃ 𝑥 𝜒 )
84 79 83 mto ⊢ ¬ 𝜓
85 6 84 bnj1541 ⊢ ( 𝜑 → 𝐹 = 𝐻 )
86 5 85 sylbir ⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐺 ‘ ⟨ 𝑥 , ( 𝐻 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) ⟩ ) ) → 𝐹 = 𝐻 )