Theorem bnj1253 35029

Description: Technical lemma for bnj60 35074. 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 34821	. . 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 35027	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑)
10	6	bnj1292 34827	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom 𝑔
11		fndm 6584	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑑 → dom 𝑔 = 𝑑)
12	10, 11	sseqtrid 3972	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑)
13		fnssres 6604	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (𝑔 ↾ 𝐷) Fn 𝐷)
14	12, 13	mpdan 687	. . . . . . . . . 10 ⊢ (𝑔 Fn 𝑑 → (𝑔 ↾ 𝐷) Fn 𝐷)
15	9, 14	bnj31 34731	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (𝑔 ↾ 𝐷) Fn 𝐷)
16	15	bnj1265 34824	. . . . . . . 8 ⊢ (𝜑 → (𝑔 ↾ 𝐷) Fn 𝐷)
17	3, 4, 5, 6, 7, 1, 8	bnj1259 35028	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑)
18	6	bnj1293 34828	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom ℎ
19		fndm 6584	. . . . . . . . . . . 12 ⊢ (ℎ Fn 𝑑 → dom ℎ = 𝑑)
20	18, 19	sseqtrid 3972	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑)
21		fnssres 6604	. . . . . . . . . . 11 ⊢ ((ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (ℎ ↾ 𝐷) Fn 𝐷)
22	20, 21	mpdan 687	. . . . . . . . . 10 ⊢ (ℎ Fn 𝑑 → (ℎ ↾ 𝐷) Fn 𝐷)
23	17, 22	bnj31 34731	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (ℎ ↾ 𝐷) Fn 𝐷)
24	23	bnj1265 34824	. . . . . . . 8 ⊢ (𝜑 → (ℎ ↾ 𝐷) Fn 𝐷)
25		ssid 3952	. . . . . . . . 9 ⊢ 𝐷 ⊆ 𝐷
26		fvreseq 6973	. . . . . . . . 9 ⊢ ((((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) ∧ 𝐷 ⊆ 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
27	25, 26	mpan2 691	. . . . . . . 8 ⊢ (((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
28	16, 24, 27	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
29		residm 5958	. . . . . . . 8 ⊢ ((𝑔 ↾ 𝐷) ↾ 𝐷) = (𝑔 ↾ 𝐷)
30		residm 5958	. . . . . . . 8 ⊢ ((ℎ ↾ 𝐷) ↾ 𝐷) = (ℎ ↾ 𝐷)
31	29, 30	eqeq12i 2749	. . . . . . 7 ⊢ (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷))
32		df-ral 3048	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
33	28, 31, 32	3bitr3g 313	. . . . . 6 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥))))
34		fvres 6841	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
35		fvres 6841	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((ℎ ↾ 𝐷)‘𝑥) = (ℎ‘𝑥))
36	34, 35	eqeq12d 2747	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
37	36	pm5.74i 271	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
38	37	albii 1820	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
39	33, 38	bitrdi 287	. . . . 5 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
40	39	necon3abid 2964	. . . 4 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
41		df-rex 3057	. . . . 5 ⊢ (∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
42		pm4.61 404	. . . . . . 7 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
43		df-ne 2929	. . . . . . . 8 ⊢ ((𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ¬ (𝑔‘𝑥) = (ℎ‘𝑥))
44	43	anbi2i 623	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
45	42, 44	bitr4i 278	. . . . . 6 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
46	45	exbii 1849	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
47		exnal 1828	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
48	41, 46, 47	3bitr2ri 300	. . . 4 ⊢ (¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
49	40, 48	bitrdi 287	. . 3 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
50	2, 49	mpbid 232	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
51	7	neeq1i 2992	. . 3 ⊢ (𝐸 ≠ ∅ ↔ {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅)
52		rabn0 4336	. . 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 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111  {cab 2709   ≠ wne 2928  ∀wral 3047  ∃wrex 3056  {crab 3395   ∩ cin 3896   ⊆ wss 3897  ∅c0 4280  ⟨cop 4579   class class class wbr 5089  dom cdm 5614   ↾ cres 5616   Fn wfn 6476  ‘cfv 6481   ∧ w-bnj17 34698   predc-bnj14 34700   FrSe w-bnj15 34704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-fv 6489  df-bnj17 34699

This theorem is referenced by:  bnj1311  35036