Theorem bnj1253 32291

Description: Technical lemma for bnj60 32336. 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 32083	. . 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 32289	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑)
10	6	bnj1292 32089	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom 𝑔
11		fndm 6457	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑑 → dom 𝑔 = 𝑑)
12	10, 11	sseqtrid 4021	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑)
13		fnssres 6472	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (𝑔 ↾ 𝐷) Fn 𝐷)
14	12, 13	mpdan 685	. . . . . . . . . 10 ⊢ (𝑔 Fn 𝑑 → (𝑔 ↾ 𝐷) Fn 𝐷)
15	9, 14	bnj31 31991	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (𝑔 ↾ 𝐷) Fn 𝐷)
16	15	bnj1265 32086	. . . . . . . 8 ⊢ (𝜑 → (𝑔 ↾ 𝐷) Fn 𝐷)
17	3, 4, 5, 6, 7, 1, 8	bnj1259 32290	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑)
18	6	bnj1293 32090	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom ℎ
19		fndm 6457	. . . . . . . . . . . 12 ⊢ (ℎ Fn 𝑑 → dom ℎ = 𝑑)
20	18, 19	sseqtrid 4021	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑)
21		fnssres 6472	. . . . . . . . . . 11 ⊢ ((ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (ℎ ↾ 𝐷) Fn 𝐷)
22	20, 21	mpdan 685	. . . . . . . . . 10 ⊢ (ℎ Fn 𝑑 → (ℎ ↾ 𝐷) Fn 𝐷)
23	17, 22	bnj31 31991	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (ℎ ↾ 𝐷) Fn 𝐷)
24	23	bnj1265 32086	. . . . . . . 8 ⊢ (𝜑 → (ℎ ↾ 𝐷) Fn 𝐷)
25		ssid 3991	. . . . . . . . 9 ⊢ 𝐷 ⊆ 𝐷
26		fvreseq 6812	. . . . . . . . 9 ⊢ ((((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) ∧ 𝐷 ⊆ 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
27	25, 26	mpan2 689	. . . . . . . 8 ⊢ (((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
28	16, 24, 27	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
29		residm 5888	. . . . . . . 8 ⊢ ((𝑔 ↾ 𝐷) ↾ 𝐷) = (𝑔 ↾ 𝐷)
30		residm 5888	. . . . . . . 8 ⊢ ((ℎ ↾ 𝐷) ↾ 𝐷) = (ℎ ↾ 𝐷)
31	29, 30	eqeq12i 2838	. . . . . . 7 ⊢ (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷))
32		df-ral 3145	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
33	28, 31, 32	3bitr3g 315	. . . . . 6 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥))))
34		fvres 6691	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
35		fvres 6691	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((ℎ ↾ 𝐷)‘𝑥) = (ℎ‘𝑥))
36	34, 35	eqeq12d 2839	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
37	36	pm5.74i 273	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
38	37	albii 1820	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
39	33, 38	syl6bb 289	. . . . 5 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
40	39	necon3abid 3054	. . . 4 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
41		df-rex 3146	. . . . 5 ⊢ (∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
42		pm4.61 407	. . . . . . 7 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
43		df-ne 3019	. . . . . . . 8 ⊢ ((𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ¬ (𝑔‘𝑥) = (ℎ‘𝑥))
44	43	anbi2i 624	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
45	42, 44	bitr4i 280	. . . . . 6 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
46	45	exbii 1848	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
47		exnal 1827	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
48	41, 46, 47	3bitr2ri 302	. . . 4 ⊢ (¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
49	40, 48	syl6bb 289	. . 3 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
50	2, 49	mpbid 234	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
51	7	neeq1i 3082	. . 3 ⊢ (𝐸 ≠ ∅ ↔ {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅)
52		rabn0 4341	. . 3 ⊢ ({𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
53	51, 52	bitri 277	. 2 ⊢ (𝐸 ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
54	50, 53	sylibr 236	1 ⊢ (𝜑 → 𝐸 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2801   ≠ wne 3018  ∀wral 3140  ∃wrex 3141  {crab 3144   ∩ cin 3937   ⊆ wss 3938  ∅c0 4293  ⟨cop 4575   class class class wbr 5068  dom cdm 5557   ↾ cres 5559   Fn wfn 6352  ‘cfv 6357   ∧ w-bnj17 31958   predc-bnj14 31960   FrSe w-bnj15 31964

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-fv 6365  df-bnj17 31959

This theorem is referenced by:  bnj1311  32298