Theorem bnj1253 31934

Description: Technical lemma for bnj60 31979. 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 31729	. . 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 31932	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑)
10	6	bnj1292 31735	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom 𝑔
11		fndm 6282	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑑 → dom 𝑔 = 𝑑)
12	10, 11	syl5sseq 3903	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑)
13		fnssres 6297	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (𝑔 ↾ 𝐷) Fn 𝐷)
14	12, 13	mpdan 674	. . . . . . . . . 10 ⊢ (𝑔 Fn 𝑑 → (𝑔 ↾ 𝐷) Fn 𝐷)
15	9, 14	bnj31 31637	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (𝑔 ↾ 𝐷) Fn 𝐷)
16	15	bnj1265 31732	. . . . . . . 8 ⊢ (𝜑 → (𝑔 ↾ 𝐷) Fn 𝐷)
17	3, 4, 5, 6, 7, 1, 8	bnj1259 31933	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑)
18	6	bnj1293 31736	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom ℎ
19		fndm 6282	. . . . . . . . . . . 12 ⊢ (ℎ Fn 𝑑 → dom ℎ = 𝑑)
20	18, 19	syl5sseq 3903	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑)
21		fnssres 6297	. . . . . . . . . . 11 ⊢ ((ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (ℎ ↾ 𝐷) Fn 𝐷)
22	20, 21	mpdan 674	. . . . . . . . . 10 ⊢ (ℎ Fn 𝑑 → (ℎ ↾ 𝐷) Fn 𝐷)
23	17, 22	bnj31 31637	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (ℎ ↾ 𝐷) Fn 𝐷)
24	23	bnj1265 31732	. . . . . . . 8 ⊢ (𝜑 → (ℎ ↾ 𝐷) Fn 𝐷)
25		ssid 3873	. . . . . . . . 9 ⊢ 𝐷 ⊆ 𝐷
26		fvreseq 6629	. . . . . . . . 9 ⊢ ((((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) ∧ 𝐷 ⊆ 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
27	25, 26	mpan2 678	. . . . . . . 8 ⊢ (((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
28	16, 24, 27	syl2anc 576	. . . . . . 7 ⊢ (𝜑 → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
29		residm 5725	. . . . . . . 8 ⊢ ((𝑔 ↾ 𝐷) ↾ 𝐷) = (𝑔 ↾ 𝐷)
30		residm 5725	. . . . . . . 8 ⊢ ((ℎ ↾ 𝐷) ↾ 𝐷) = (ℎ ↾ 𝐷)
31	29, 30	eqeq12i 2786	. . . . . . 7 ⊢ (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷))
32		df-ral 3087	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
33	28, 31, 32	3bitr3g 305	. . . . . 6 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥))))
34		fvres 6512	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
35		fvres 6512	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((ℎ ↾ 𝐷)‘𝑥) = (ℎ‘𝑥))
36	34, 35	eqeq12d 2787	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
37	36	pm5.74i 263	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
38	37	albii 1782	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
39	33, 38	syl6bb 279	. . . . 5 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
40	39	necon3abid 2997	. . . 4 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
41		df-rex 3088	. . . . 5 ⊢ (∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
42		pm4.61 396	. . . . . . 7 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
43		df-ne 2962	. . . . . . . 8 ⊢ ((𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ¬ (𝑔‘𝑥) = (ℎ‘𝑥))
44	43	anbi2i 613	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
45	42, 44	bitr4i 270	. . . . . 6 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
46	45	exbii 1810	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
47		exnal 1789	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
48	41, 46, 47	3bitr2ri 292	. . . 4 ⊢ (¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
49	40, 48	syl6bb 279	. . 3 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
50	2, 49	mpbid 224	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
51	7	neeq1i 3025	. . 3 ⊢ (𝐸 ≠ ∅ ↔ {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅)
52		rabn0 4219	. . 3 ⊢ ({𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
53	51, 52	bitri 267	. 2 ⊢ (𝐸 ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
54	50, 53	sylibr 226	1 ⊢ (𝜑 → 𝐸 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068  ∀wal 1505   = wceq 1507  ∃wex 1742   ∈ wcel 2050  {cab 2752   ≠ wne 2961  ∀wral 3082  ∃wrex 3083  {crab 3086   ∩ cin 3822   ⊆ wss 3823  ∅c0 4172  ⟨cop 4441   class class class wbr 4923  dom cdm 5401   ↾ cres 5403   Fn wfn 6177  ‘cfv 6182   ∧ w-bnj17 31604   predc-bnj14 31606   FrSe w-bnj15 31610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-iota 6146  df-fun 6184  df-fn 6185  df-fv 6190  df-bnj17 31605

This theorem is referenced by:  bnj1311  31941