Theorem fnwelem 7557

Description: Lemma for fnwe 7558. (Contributed by Mario Carneiro, 10-Mar-2013.) (Revised by Mario Carneiro, 18-Nov-2014.)

Hypotheses

Ref	Expression
fnwe.1	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))}
fnwe.2	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fnwe.3	⊢ (𝜑 → 𝑅 We 𝐵)
fnwe.4	⊢ (𝜑 → 𝑆 We 𝐴)
fnwe.5	⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V)
fnwelem.6	⊢ 𝑄 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣))))}
fnwelem.7	⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ ⟨(𝐹‘𝑧), 𝑧⟩)

Assertion

Ref	Expression
fnwelem	⊢ (𝜑 → 𝑇 We 𝐴)

Distinct variable groups:   𝑣,𝑢,𝑤,𝑥,𝑦,𝑧,𝐴   𝑢,𝐵,𝑣,𝑤,𝑥,𝑦,𝑧   𝑤,𝐺,𝑥,𝑦   𝜑,𝑤,𝑥,𝑧   𝑢,𝐹,𝑣,𝑤,𝑥,𝑦,𝑧   𝑤,𝑄,𝑥,𝑦   𝑢,𝑅,𝑣,𝑤,𝑥,𝑦   𝑢,𝑆,𝑣,𝑤,𝑥,𝑦   𝑤,𝑇

Allowed substitution hints:   𝜑(𝑦,𝑣,𝑢)   𝑄(𝑧,𝑣,𝑢)   𝑅(𝑧)   𝑆(𝑧)   𝑇(𝑥,𝑦,𝑧,𝑣,𝑢)   𝐺(𝑧,𝑣,𝑢)

Proof of Theorem fnwelem

Step	Hyp	Ref	Expression
1		fnwe.2	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffvelrn 6607	. . . . . 6 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵)
3		simpr 479	. . . . . 6 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴)
4	2, 3	opelxpd 5381	. . . . 5 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → ⟨(𝐹‘𝑧), 𝑧⟩ ∈ (𝐵 × 𝐴))
5		fnwelem.7	. . . . 5 ⊢ 𝐺 = (𝑧 ∈ 𝐴 ↦ ⟨(𝐹‘𝑧), 𝑧⟩)
6	4, 5	fmptd 6634	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → 𝐺:𝐴⟶(𝐵 × 𝐴))
7		frn 6285	. . . 4 ⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → ran 𝐺 ⊆ (𝐵 × 𝐴))
8	1, 6, 7	3syl 18	. . 3 ⊢ (𝜑 → ran 𝐺 ⊆ (𝐵 × 𝐴))
9		fnwe.3	. . . 4 ⊢ (𝜑 → 𝑅 We 𝐵)
10		fnwe.4	. . . 4 ⊢ (𝜑 → 𝑆 We 𝐴)
11		fnwelem.6	. . . . 5 ⊢ 𝑄 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣))))}
12	11	wexp 7556	. . . 4 ⊢ ((𝑅 We 𝐵 ∧ 𝑆 We 𝐴) → 𝑄 We (𝐵 × 𝐴))
13	9, 10, 12	syl2anc 581	. . 3 ⊢ (𝜑 → 𝑄 We (𝐵 × 𝐴))
14		wess 5330	. . 3 ⊢ (ran 𝐺 ⊆ (𝐵 × 𝐴) → (𝑄 We (𝐵 × 𝐴) → 𝑄 We ran 𝐺))
15	8, 13, 14	sylc 65	. 2 ⊢ (𝜑 → 𝑄 We ran 𝐺)
16		fveq2 6434	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥))
17		id 22	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥)
18	16, 17	opeq12d 4632	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ⟨(𝐹‘𝑧), 𝑧⟩ = ⟨(𝐹‘𝑥), 𝑥⟩)
19		opex 5154	. . . . . . . . . . 11 ⊢ ⟨(𝐹‘𝑥), 𝑥⟩ ∈ V
20	18, 5, 19	fvmpt 6530	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐴 → (𝐺‘𝑥) = ⟨(𝐹‘𝑥), 𝑥⟩)
21		fveq2 6434	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦))
22		id 22	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → 𝑧 = 𝑦)
23	21, 22	opeq12d 4632	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ⟨(𝐹‘𝑧), 𝑧⟩ = ⟨(𝐹‘𝑦), 𝑦⟩)
24		opex 5154	. . . . . . . . . . 11 ⊢ ⟨(𝐹‘𝑦), 𝑦⟩ ∈ V
25	23, 5, 24	fvmpt 6530	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝐴 → (𝐺‘𝑦) = ⟨(𝐹‘𝑦), 𝑦⟩)
26	20, 25	eqeqan12d 2842	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑥) = (𝐺‘𝑦) ↔ ⟨(𝐹‘𝑥), 𝑥⟩ = ⟨(𝐹‘𝑦), 𝑦⟩))
27		fvex 6447	. . . . . . . . . . 11 ⊢ (𝐹‘𝑥) ∈ V
28		vex 3418	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
29	27, 28	opth 5166	. . . . . . . . . 10 ⊢ (⟨(𝐹‘𝑥), 𝑥⟩ = ⟨(𝐹‘𝑦), 𝑦⟩ ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 = 𝑦))
30	29	simprbi 492	. . . . . . . . 9 ⊢ (⟨(𝐹‘𝑥), 𝑥⟩ = ⟨(𝐹‘𝑦), 𝑦⟩ → 𝑥 = 𝑦)
31	26, 30	syl6bi 245	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑥) = (𝐺‘𝑦) → 𝑥 = 𝑦))
32	31	rgen2a 3187	. . . . . . 7 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐺‘𝑥) = (𝐺‘𝑦) → 𝑥 = 𝑦)
33		dff13 6768	. . . . . . 7 ⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) ↔ (𝐺:𝐴⟶(𝐵 × 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐺‘𝑥) = (𝐺‘𝑦) → 𝑥 = 𝑦)))
34	6, 32, 33	sylanblrc 586	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → 𝐺:𝐴–1-1→(𝐵 × 𝐴))
35		f1f1orn 6390	. . . . . 6 ⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) → 𝐺:𝐴–1-1-onto→ran 𝐺)
36		f1ocnv 6391	. . . . . 6 ⊢ (𝐺:𝐴–1-1-onto→ran 𝐺 → ◡𝐺:ran 𝐺–1-1-onto→𝐴)
37	1, 34, 35, 36	4syl 19	. . . . 5 ⊢ (𝜑 → ◡𝐺:ran 𝐺–1-1-onto→𝐴)
38		eqid 2826	. . . . . . 7 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))}
39	38	f1oiso2 6858	. . . . . 6 ⊢ (◡𝐺:ran 𝐺–1-1-onto→𝐴 → ◡𝐺 Isom 𝑄, {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} (ran 𝐺, 𝐴))
40		fnwe.1	. . . . . . . 8 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))}
41		frel 6284	. . . . . . . . . . . . . . . 16 ⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → Rel 𝐺)
42		dfrel2 5825	. . . . . . . . . . . . . . . 16 ⊢ (Rel 𝐺 ↔ ◡◡𝐺 = 𝐺)
43	41, 42	sylib 210	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → ◡◡𝐺 = 𝐺)
44	43	fveq1d 6436	. . . . . . . . . . . . . 14 ⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → (◡◡𝐺‘𝑥) = (𝐺‘𝑥))
45	43	fveq1d 6436	. . . . . . . . . . . . . 14 ⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → (◡◡𝐺‘𝑦) = (𝐺‘𝑦))
46	44, 45	breq12d 4887	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐴⟶(𝐵 × 𝐴) → ((◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦) ↔ (𝐺‘𝑥)𝑄(𝐺‘𝑦)))
47	6, 46	syl 17	. . . . . . . . . . . 12 ⊢ (𝐹:𝐴⟶𝐵 → ((◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦) ↔ (𝐺‘𝑥)𝑄(𝐺‘𝑦)))
48	47	adantr 474	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦) ↔ (𝐺‘𝑥)𝑄(𝐺‘𝑦)))
49	20, 25	breqan12d 4890	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐺‘𝑥)𝑄(𝐺‘𝑦) ↔ ⟨(𝐹‘𝑥), 𝑥⟩𝑄⟨(𝐹‘𝑦), 𝑦⟩))
50	49	adantl 475	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝐺‘𝑥)𝑄(𝐺‘𝑦) ↔ ⟨(𝐹‘𝑥), 𝑥⟩𝑄⟨(𝐹‘𝑦), 𝑦⟩))
51		ffvelrn 6607	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵)
52		simpr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴)
53	51, 52	jca 509	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
54		ffvelrn 6607	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ 𝐵)
55		simpr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴)
56	54, 55	jca 509	. . . . . . . . . . . . . 14 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
57	53, 56	anim12dan 614	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))
58	57	biantrurd 530	. . . . . . . . . . . 12 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)) ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))))
59		eleq1 2895	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → (𝑢 ∈ (𝐵 × 𝐴) ↔ ⟨(𝐹‘𝑥), 𝑥⟩ ∈ (𝐵 × 𝐴)))
60		opelxp 5379	. . . . . . . . . . . . . . . 16 ⊢ (⟨(𝐹‘𝑥), 𝑥⟩ ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴))
61	59, 60	syl6bb 279	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → (𝑢 ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)))
62	61	anbi1d 625	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → ((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ↔ (((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴))))
63	27, 28	op1std 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → (1st ‘𝑢) = (𝐹‘𝑥))
64	63	breq1d 4884	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → ((1st ‘𝑢)𝑅(1st ‘𝑣) ↔ (𝐹‘𝑥)𝑅(1st ‘𝑣)))
65	63	eqeq1d 2828	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → ((1st ‘𝑢) = (1st ‘𝑣) ↔ (𝐹‘𝑥) = (1st ‘𝑣)))
66	27, 28	op2ndd 7440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → (2nd ‘𝑢) = 𝑥)
67	66	breq1d 4884	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → ((2nd ‘𝑢)𝑆(2nd ‘𝑣) ↔ 𝑥𝑆(2nd ‘𝑣)))
68	65, 67	anbi12d 626	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → (((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣)) ↔ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣))))
69	64, 68	orbi12d 949	. . . . . . . . . . . . . 14 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → (((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣))) ↔ ((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣)))))
70	62, 69	anbi12d 626	. . . . . . . . . . . . 13 ⊢ (𝑢 = ⟨(𝐹‘𝑥), 𝑥⟩ → (((𝑢 ∈ (𝐵 × 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((1st ‘𝑢)𝑅(1st ‘𝑣) ∨ ((1st ‘𝑢) = (1st ‘𝑣) ∧ (2nd ‘𝑢)𝑆(2nd ‘𝑣)))) ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣))))))
71		eleq1 2895	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (𝑣 ∈ (𝐵 × 𝐴) ↔ ⟨(𝐹‘𝑦), 𝑦⟩ ∈ (𝐵 × 𝐴)))
72		opelxp 5379	. . . . . . . . . . . . . . . 16 ⊢ (⟨(𝐹‘𝑦), 𝑦⟩ ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))
73	71, 72	syl6bb 279	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (𝑣 ∈ (𝐵 × 𝐴) ↔ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)))
74	73	anbi2d 624	. . . . . . . . . . . . . 14 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ↔ (((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴))))
75		fvex 6447	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹‘𝑦) ∈ V
76		vex 3418	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
77	75, 76	op1std 7439	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (1st ‘𝑣) = (𝐹‘𝑦))
78	77	breq2d 4886	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → ((𝐹‘𝑥)𝑅(1st ‘𝑣) ↔ (𝐹‘𝑥)𝑅(𝐹‘𝑦)))
79	77	eqeq2d 2836	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → ((𝐹‘𝑥) = (1st ‘𝑣) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
80	75, 76	op2ndd 7440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (2nd ‘𝑣) = 𝑦)
81	80	breq2d 4886	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (𝑥𝑆(2nd ‘𝑣) ↔ 𝑥𝑆𝑦))
82	79, 81	anbi12d 626	. . . . . . . . . . . . . . 15 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣)) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))
83	78, 82	orbi12d 949	. . . . . . . . . . . . . 14 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣))) ↔ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))))
84	74, 83	anbi12d 626	. . . . . . . . . . . . 13 ⊢ (𝑣 = ⟨(𝐹‘𝑦), 𝑦⟩ → (((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑣 ∈ (𝐵 × 𝐴)) ∧ ((𝐹‘𝑥)𝑅(1st ‘𝑣) ∨ ((𝐹‘𝑥) = (1st ‘𝑣) ∧ 𝑥𝑆(2nd ‘𝑣)))) ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))))
85	19, 24, 70, 84, 11	brab 5225	. . . . . . . . . . . 12 ⊢ (⟨(𝐹‘𝑥), 𝑥⟩𝑄⟨(𝐹‘𝑦), 𝑦⟩ ↔ ((((𝐹‘𝑥) ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ ((𝐹‘𝑦) ∈ 𝐵 ∧ 𝑦 ∈ 𝐴)) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))))
86	58, 85	syl6rbbr 282	. . . . . . . . . . 11 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (⟨(𝐹‘𝑥), 𝑥⟩𝑄⟨(𝐹‘𝑦), 𝑦⟩ ↔ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))))
87	48, 50, 86	3bitrrd 298	. . . . . . . . . 10 ⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)) ↔ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦)))
88	87	pm5.32da 576	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))))
89	88	opabbidv 4940	. . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑆𝑦)))} = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))})
90	40, 89	syl5eq 2874	. . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))})
91		isoeq3 6825	. . . . . . 7 ⊢ (𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} → (◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴) ↔ ◡𝐺 Isom 𝑄, {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} (ran 𝐺, 𝐴)))
92	90, 91	syl 17	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴) ↔ ◡𝐺 Isom 𝑄, {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (◡◡𝐺‘𝑥)𝑄(◡◡𝐺‘𝑦))} (ran 𝐺, 𝐴)))
93	39, 92	syl5ibr 238	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐺:ran 𝐺–1-1-onto→𝐴 → ◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴)))
94	1, 37, 93	sylc 65	. . . 4 ⊢ (𝜑 → ◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴))
95		isocnv 6836	. . . 4 ⊢ (◡𝐺 Isom 𝑄, 𝑇 (ran 𝐺, 𝐴) → ◡◡𝐺 Isom 𝑇, 𝑄 (𝐴, ran 𝐺))
96	94, 95	syl 17	. . 3 ⊢ (𝜑 → ◡◡𝐺 Isom 𝑇, 𝑄 (𝐴, ran 𝐺))
97		imacnvcnv 5841	. . . . 5 ⊢ (◡◡𝐺 “ 𝑤) = (𝐺 “ 𝑤)
98		fnwe.5	. . . . . . 7 ⊢ (𝜑 → (𝐹 “ 𝑤) ∈ V)
99		vex 3418	. . . . . . 7 ⊢ 𝑤 ∈ V
100		xpexg 7221	. . . . . . 7 ⊢ (((𝐹 “ 𝑤) ∈ V ∧ 𝑤 ∈ V) → ((𝐹 “ 𝑤) × 𝑤) ∈ V)
101	98, 99, 100	sylancl 582	. . . . . 6 ⊢ (𝜑 → ((𝐹 “ 𝑤) × 𝑤) ∈ V)
102		imadmres 5869	. . . . . . 7 ⊢ (𝐺 “ dom (𝐺 ↾ 𝑤)) = (𝐺 “ 𝑤)
103		dmres 5656	. . . . . . . . . . 11 ⊢ dom (𝐺 ↾ 𝑤) = (𝑤 ∩ dom 𝐺)
104	103	elin2 4029	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom (𝐺 ↾ 𝑤) ↔ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺))
105		simprr 791	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ dom 𝐺)
106		f1dm 6343	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) → dom 𝐺 = 𝐴)
107	1, 34, 106	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝐴)
108	107	adantr 474	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → dom 𝐺 = 𝐴)
109	105, 108	eleqtrd 2909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ 𝐴)
110	109, 20	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐺‘𝑥) = ⟨(𝐹‘𝑥), 𝑥⟩)
111	1	ffnd 6280	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn 𝐴)
112	111	adantr 474	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝐹 Fn 𝐴)
113		dmres 5656	. . . . . . . . . . . . . . 15 ⊢ dom (𝐹 ↾ 𝑤) = (𝑤 ∩ dom 𝐹)
114		inss2 4059	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 ∩ dom 𝐹) ⊆ dom 𝐹
115		fndm 6224	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
116	112, 115	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → dom 𝐹 = 𝐴)
117	114, 116	syl5sseq 3879	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝑤 ∩ dom 𝐹) ⊆ 𝐴)
118	113, 117	syl5eqss 3875	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → dom (𝐹 ↾ 𝑤) ⊆ 𝐴)
119		simprl 789	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ 𝑤)
120	109, 116	eleqtrrd 2910	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ dom 𝐹)
121	113	elin2 4029	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ dom (𝐹 ↾ 𝑤) ↔ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐹))
122	119, 120, 121	sylanbrc 580	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → 𝑥 ∈ dom (𝐹 ↾ 𝑤))
123		fnfvima 6753	. . . . . . . . . . . . . 14 ⊢ ((𝐹 Fn 𝐴 ∧ dom (𝐹 ↾ 𝑤) ⊆ 𝐴 ∧ 𝑥 ∈ dom (𝐹 ↾ 𝑤)) → (𝐹‘𝑥) ∈ (𝐹 “ dom (𝐹 ↾ 𝑤)))
124	112, 118, 122, 123	syl3anc 1496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐹‘𝑥) ∈ (𝐹 “ dom (𝐹 ↾ 𝑤)))
125		imadmres 5869	. . . . . . . . . . . . 13 ⊢ (𝐹 “ dom (𝐹 ↾ 𝑤)) = (𝐹 “ 𝑤)
126	124, 125	syl6eleq 2917	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑤))
127	126, 119	opelxpd 5381	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → ⟨(𝐹‘𝑥), 𝑥⟩ ∈ ((𝐹 “ 𝑤) × 𝑤))
128	110, 127	eqeltrd 2907	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑤 ∧ 𝑥 ∈ dom 𝐺)) → (𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤))
129	104, 128	sylan2b 589	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ dom (𝐺 ↾ 𝑤)) → (𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤))
130	129	ralrimiva 3176	. . . . . . . 8 ⊢ (𝜑 → ∀𝑥 ∈ dom (𝐺 ↾ 𝑤)(𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤))
131		f1fun 6341	. . . . . . . . . 10 ⊢ (𝐺:𝐴–1-1→(𝐵 × 𝐴) → Fun 𝐺)
132	1, 34, 131	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → Fun 𝐺)
133		resss 5659	. . . . . . . . . 10 ⊢ (𝐺 ↾ 𝑤) ⊆ 𝐺
134		dmss 5556	. . . . . . . . . 10 ⊢ ((𝐺 ↾ 𝑤) ⊆ 𝐺 → dom (𝐺 ↾ 𝑤) ⊆ dom 𝐺)
135	133, 134	ax-mp 5	. . . . . . . . 9 ⊢ dom (𝐺 ↾ 𝑤) ⊆ dom 𝐺
136		funimass4 6495	. . . . . . . . 9 ⊢ ((Fun 𝐺 ∧ dom (𝐺 ↾ 𝑤) ⊆ dom 𝐺) → ((𝐺 “ dom (𝐺 ↾ 𝑤)) ⊆ ((𝐹 “ 𝑤) × 𝑤) ↔ ∀𝑥 ∈ dom (𝐺 ↾ 𝑤)(𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤)))
137	132, 135, 136	sylancl 582	. . . . . . . 8 ⊢ (𝜑 → ((𝐺 “ dom (𝐺 ↾ 𝑤)) ⊆ ((𝐹 “ 𝑤) × 𝑤) ↔ ∀𝑥 ∈ dom (𝐺 ↾ 𝑤)(𝐺‘𝑥) ∈ ((𝐹 “ 𝑤) × 𝑤)))
138	130, 137	mpbird 249	. . . . . . 7 ⊢ (𝜑 → (𝐺 “ dom (𝐺 ↾ 𝑤)) ⊆ ((𝐹 “ 𝑤) × 𝑤))
139	102, 138	syl5eqssr 3876	. . . . . 6 ⊢ (𝜑 → (𝐺 “ 𝑤) ⊆ ((𝐹 “ 𝑤) × 𝑤))
140	101, 139	ssexd 5031	. . . . 5 ⊢ (𝜑 → (𝐺 “ 𝑤) ∈ V)
141	97, 140	syl5eqel 2911	. . . 4 ⊢ (𝜑 → (◡◡𝐺 “ 𝑤) ∈ V)
142	141	alrimiv 2028	. . 3 ⊢ (𝜑 → ∀𝑤(◡◡𝐺 “ 𝑤) ∈ V)
143		isowe2 6856	. . 3 ⊢ ((◡◡𝐺 Isom 𝑇, 𝑄 (𝐴, ran 𝐺) ∧ ∀𝑤(◡◡𝐺 “ 𝑤) ∈ V) → (𝑄 We ran 𝐺 → 𝑇 We 𝐴))
144	96, 142, 143	syl2anc 581	. 2 ⊢ (𝜑 → (𝑄 We ran 𝐺 → 𝑇 We 𝐴))
145	15, 144	mpd 15	1 ⊢ (𝜑 → 𝑇 We 𝐴)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∨ wo 880  ∀wal 1656   = wceq 1658   ∈ wcel 2166  ∀wral 3118  Vcvv 3415   ∩ cin 3798   ⊆ wss 3799  ⟨cop 4404   class class class wbr 4874  {copab 4936   ↦ cmpt 4953   We wwe 5301   × cxp 5341  ^◡ccnv 5342  dom cdm 5343  ran crn 5344   ↾ cres 5345   “ cima 5346  Rel wrel 5348  Fun wfun 6118   Fn wfn 6119  ⟶wf 6120  –1-1→wf1 6121  –1-1-onto→wf1o 6123  ‘cfv 6124   Isom wiso 6125  1^st c1st 7427  2^nd c2nd 7428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rex 3124  df-rab 3127  df-v 3417  df-sbc 3664  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4660  df-int 4699  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-po 5264  df-so 5265  df-fr 5302  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-1st 7429  df-2nd 7430

This theorem is referenced by:  fnwe  7558