Theorem bnj1253 35053

Description: Technical lemma for bnj60 35098. 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.)

Hypotheses

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

Assertion

Ref	Expression
bnj1253	⊢ (𝜑 → 𝐸 ≠ ∅)

Distinct variable groups:   𝐴,𝑓   𝐵,𝑓,𝑔   𝐵,ℎ,𝑓   𝐷,𝑑   𝑥,𝐷   𝑓,𝐺,𝑔   ℎ,𝐺   𝑅,𝑓   𝑔,𝑌   ℎ,𝑌   𝑓,𝑑,𝑔   ℎ,𝑑   𝑥,𝑓,𝑔   𝑥,ℎ

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑔,ℎ,𝑑)   𝜓(𝑥,𝑦,𝑓,𝑔,ℎ,𝑑)   𝐴(𝑥,𝑦,𝑔,ℎ,𝑑)   𝐵(𝑥,𝑦,𝑑)   𝐶(𝑥,𝑦,𝑓,𝑔,ℎ,𝑑)   𝐷(𝑦,𝑓,𝑔,ℎ)   𝑅(𝑥,𝑦,𝑔,ℎ,𝑑)   𝐸(𝑥,𝑦,𝑓,𝑔,ℎ,𝑑)   𝐺(𝑥,𝑦,𝑑)   𝑌(𝑥,𝑦,𝑓,𝑑)

Proof of Theorem bnj1253

Step	Hyp	Ref	Expression
1		bnj1253.6	. . . 4 ⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷)))
2	1	bnj1254 34845	. . 3 ⊢ (𝜑 → (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))
3		bnj1253.1	. . . . . . . . . . 11 ⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}
4		bnj1253.2	. . . . . . . . . . 11 ⊢ 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩
5		bnj1253.3	. . . . . . . . . . 11 ⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))}
6		bnj1253.4	. . . . . . . . . . 11 ⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ)
7		bnj1253.5	. . . . . . . . . . 11 ⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)}
8		bnj1253.7	. . . . . . . . . . 11 ⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥))
9	3, 4, 5, 6, 7, 1, 8	bnj1256 35051	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑)
10	6	bnj1292 34851	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom 𝑔
11		fndm 6646	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑑 → dom 𝑔 = 𝑑)
12	10, 11	sseqtrid 4006	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑)
13		fnssres 6666	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (𝑔 ↾ 𝐷) Fn 𝐷)
14	12, 13	mpdan 687	. . . . . . . . . 10 ⊢ (𝑔 Fn 𝑑 → (𝑔 ↾ 𝐷) Fn 𝐷)
15	9, 14	bnj31 34755	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (𝑔 ↾ 𝐷) Fn 𝐷)
16	15	bnj1265 34848	. . . . . . . 8 ⊢ (𝜑 → (𝑔 ↾ 𝐷) Fn 𝐷)
17	3, 4, 5, 6, 7, 1, 8	bnj1259 35052	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑)
18	6	bnj1293 34852	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom ℎ
19		fndm 6646	. . . . . . . . . . . 12 ⊢ (ℎ Fn 𝑑 → dom ℎ = 𝑑)
20	18, 19	sseqtrid 4006	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑)
21		fnssres 6666	. . . . . . . . . . 11 ⊢ ((ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (ℎ ↾ 𝐷) Fn 𝐷)
22	20, 21	mpdan 687	. . . . . . . . . 10 ⊢ (ℎ Fn 𝑑 → (ℎ ↾ 𝐷) Fn 𝐷)
23	17, 22	bnj31 34755	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (ℎ ↾ 𝐷) Fn 𝐷)
24	23	bnj1265 34848	. . . . . . . 8 ⊢ (𝜑 → (ℎ ↾ 𝐷) Fn 𝐷)
25		ssid 3986	. . . . . . . . 9 ⊢ 𝐷 ⊆ 𝐷
26		fvreseq 7035	. . . . . . . . 9 ⊢ ((((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) ∧ 𝐷 ⊆ 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
27	25, 26	mpan2 691	. . . . . . . 8 ⊢ (((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
28	16, 24, 27	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
29		residm 6002	. . . . . . . 8 ⊢ ((𝑔 ↾ 𝐷) ↾ 𝐷) = (𝑔 ↾ 𝐷)
30		residm 6002	. . . . . . . 8 ⊢ ((ℎ ↾ 𝐷) ↾ 𝐷) = (ℎ ↾ 𝐷)
31	29, 30	eqeq12i 2754	. . . . . . 7 ⊢ (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷))
32		df-ral 3053	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
33	28, 31, 32	3bitr3g 313	. . . . . 6 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥))))
34		fvres 6900	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
35		fvres 6900	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((ℎ ↾ 𝐷)‘𝑥) = (ℎ‘𝑥))
36	34, 35	eqeq12d 2752	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
37	36	pm5.74i 271	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
38	37	albii 1819	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
39	33, 38	bitrdi 287	. . . . 5 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
40	39	necon3abid 2969	. . . 4 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
41		df-rex 3062	. . . . 5 ⊢ (∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
42		pm4.61 404	. . . . . . 7 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
43		df-ne 2934	. . . . . . . 8 ⊢ ((𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ¬ (𝑔‘𝑥) = (ℎ‘𝑥))
44	43	anbi2i 623	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
45	42, 44	bitr4i 278	. . . . . 6 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
46	45	exbii 1848	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
47		exnal 1827	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
48	41, 46, 47	3bitr2ri 300	. . . 4 ⊢ (¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
49	40, 48	bitrdi 287	. . 3 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
50	2, 49	mpbid 232	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
51	7	neeq1i 2997	. . 3 ⊢ (𝐸 ≠ ∅ ↔ {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅)
52		rabn0 4369	. . 3 ⊢ ({𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
53	51, 52	bitri 275	. 2 ⊢ (𝐸 ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
54	50, 53	sylibr 234	1 ⊢ (𝜑 → 𝐸 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2714   ≠ wne 2933  ∀wral 3052  ∃wrex 3061  {crab 3420   ∩ cin 3930   ⊆ wss 3931  ∅c0 4313  ⟨cop 4612   class class class wbr 5124  dom cdm 5659   ↾ cres 5661   Fn wfn 6531  ‘cfv 6536   ∧ w-bnj17 34722   predc-bnj14 34724   FrSe w-bnj15 34728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-fv 6544  df-bnj17 34723

This theorem is referenced by:  bnj1311  35060