Theorem bnj1253 34016

Description: Technical lemma for bnj60 34061. 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 33808	. . 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 34014	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑)
10	6	bnj1292 33814	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom 𝑔
11		fndm 6649	. . . . . . . . . . . 12 ⊢ (𝑔 Fn 𝑑 → dom 𝑔 = 𝑑)
12	10, 11	sseqtrid 4033	. . . . . . . . . . 11 ⊢ (𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑)
13		fnssres 6670	. . . . . . . . . . 11 ⊢ ((𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (𝑔 ↾ 𝐷) Fn 𝐷)
14	12, 13	mpdan 685	. . . . . . . . . 10 ⊢ (𝑔 Fn 𝑑 → (𝑔 ↾ 𝐷) Fn 𝐷)
15	9, 14	bnj31 33718	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (𝑔 ↾ 𝐷) Fn 𝐷)
16	15	bnj1265 33811	. . . . . . . 8 ⊢ (𝜑 → (𝑔 ↾ 𝐷) Fn 𝐷)
17	3, 4, 5, 6, 7, 1, 8	bnj1259 34015	. . . . . . . . . 10 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑)
18	6	bnj1293 33815	. . . . . . . . . . . 12 ⊢ 𝐷 ⊆ dom ℎ
19		fndm 6649	. . . . . . . . . . . 12 ⊢ (ℎ Fn 𝑑 → dom ℎ = 𝑑)
20	18, 19	sseqtrid 4033	. . . . . . . . . . 11 ⊢ (ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑)
21		fnssres 6670	. . . . . . . . . . 11 ⊢ ((ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (ℎ ↾ 𝐷) Fn 𝐷)
22	20, 21	mpdan 685	. . . . . . . . . 10 ⊢ (ℎ Fn 𝑑 → (ℎ ↾ 𝐷) Fn 𝐷)
23	17, 22	bnj31 33718	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (ℎ ↾ 𝐷) Fn 𝐷)
24	23	bnj1265 33811	. . . . . . . 8 ⊢ (𝜑 → (ℎ ↾ 𝐷) Fn 𝐷)
25		ssid 4003	. . . . . . . . 9 ⊢ 𝐷 ⊆ 𝐷
26		fvreseq 7038	. . . . . . . . 9 ⊢ ((((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) ∧ 𝐷 ⊆ 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
27	25, 26	mpan2 689	. . . . . . . 8 ⊢ (((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
28	16, 24, 27	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ ∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
29		residm 6012	. . . . . . . 8 ⊢ ((𝑔 ↾ 𝐷) ↾ 𝐷) = (𝑔 ↾ 𝐷)
30		residm 6012	. . . . . . . 8 ⊢ ((ℎ ↾ 𝐷) ↾ 𝐷) = (ℎ ↾ 𝐷)
31	29, 30	eqeq12i 2750	. . . . . . 7 ⊢ (((𝑔 ↾ 𝐷) ↾ 𝐷) = ((ℎ ↾ 𝐷) ↾ 𝐷) ↔ (𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷))
32		df-ral 3062	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐷 ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)))
33	28, 31, 32	3bitr3g 312	. . . . . 6 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥))))
34		fvres 6907	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = (𝑔‘𝑥))
35		fvres 6907	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐷 → ((ℎ ↾ 𝐷)‘𝑥) = (ℎ‘𝑥))
36	34, 35	eqeq12d 2748	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐷 → (((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥) ↔ (𝑔‘𝑥) = (ℎ‘𝑥)))
37	36	pm5.74i 270	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
38	37	albii 1821	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑥) = ((ℎ ↾ 𝐷)‘𝑥)) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
39	33, 38	bitrdi 286	. . . . 5 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) = (ℎ ↾ 𝐷) ↔ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
40	39	necon3abid 2977	. . . 4 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥))))
41		df-rex 3071	. . . . 5 ⊢ (∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
42		pm4.61 405	. . . . . . 7 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
43		df-ne 2941	. . . . . . . 8 ⊢ ((𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ ¬ (𝑔‘𝑥) = (ℎ‘𝑥))
44	43	anbi2i 623	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ ¬ (𝑔‘𝑥) = (ℎ‘𝑥)))
45	42, 44	bitr4i 277	. . . . . 6 ⊢ (¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ (𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
46	45	exbii 1850	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥(𝑥 ∈ 𝐷 ∧ (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
47		exnal 1829	. . . . 5 ⊢ (∃𝑥 ¬ (𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)))
48	41, 46, 47	3bitr2ri 299	. . . 4 ⊢ (¬ ∀𝑥(𝑥 ∈ 𝐷 → (𝑔‘𝑥) = (ℎ‘𝑥)) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
49	40, 48	bitrdi 286	. . 3 ⊢ (𝜑 → ((𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷) ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥)))
50	2, 49	mpbid 231	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
51	7	neeq1i 3005	. . 3 ⊢ (𝐸 ≠ ∅ ↔ {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅)
52		rabn0 4384	. . 3 ⊢ ({𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
53	51, 52	bitri 274	. 2 ⊢ (𝐸 ≠ ∅ ↔ ∃𝑥 ∈ 𝐷 (𝑔‘𝑥) ≠ (ℎ‘𝑥))
54	50, 53	sylibr 233	1 ⊢ (𝜑 → 𝐸 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2709   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3432   ∩ cin 3946   ⊆ wss 3947  ∅c0 4321  ⟨cop 4633   class class class wbr 5147  dom cdm 5675   ↾ cres 5677   Fn wfn 6535  ‘cfv 6540   ∧ w-bnj17 33685   predc-bnj14 33687   FrSe w-bnj15 33691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-fv 6548  df-bnj17 33686

This theorem is referenced by:  bnj1311  34023