Theorem wemapsolem 9318

Description: Lemma for wemapso 9319. (Contributed by Stefan O'Rear, 18-Jan-2015.) (Revised by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 21-Jul-2024.)

Hypotheses

Ref	Expression
wemapso.t	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
wemapsolem.1	⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴)
wemapsolem.2	⊢ (𝜑 → 𝑅 Or 𝐴)
wemapsolem.3	⊢ (𝜑 → 𝑆 Or 𝐵)
wemapsolem.4	⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)

Assertion

Ref	Expression
wemapsolem	⊢ (𝜑 → 𝑇 Or 𝑈)

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝐵   𝑇,𝑎,𝑏,𝑐,𝑑   𝑈,𝑎,𝑏,𝑐,𝑑   𝑤,𝑎,𝑦,𝑧,𝑏,𝑐,𝑥,𝐴,𝑑   𝑅,𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧   𝑆,𝑎,𝑏,𝑐,𝑑,𝑤,𝑥,𝑦,𝑧   𝜑,𝑎,𝑏,𝑐,𝑑

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝐵(𝑦,𝑧,𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤)   𝑈(𝑥,𝑦,𝑧,𝑤)

Proof of Theorem wemapsolem

Step	Hyp	Ref	Expression
1		wemapsolem.1	. . 3 ⊢ 𝑈 ⊆ (𝐵 ↑m 𝐴)
2		wemapsolem.2	. . . 4 ⊢ (𝜑 → 𝑅 Or 𝐴)
3		wemapsolem.3	. . . . 5 ⊢ (𝜑 → 𝑆 Or 𝐵)
4		sopo 5523	. . . . 5 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝑆 Po 𝐵)
6		wemapso.t	. . . . 5 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
7	6	wemappo 9317	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴))
8	2, 5, 7	syl2anc 584	. . 3 ⊢ (𝜑 → 𝑇 Po (𝐵 ↑m 𝐴))
9		poss 5506	. . 3 ⊢ (𝑈 ⊆ (𝐵 ↑m 𝐴) → (𝑇 Po (𝐵 ↑m 𝐴) → 𝑇 Po 𝑈))
10	1, 8, 9	mpsyl 68	. 2 ⊢ (𝜑 → 𝑇 Po 𝑈)
11		df-ne 2945	. . . . 5 ⊢ (𝑎 ≠ 𝑏 ↔ ¬ 𝑎 = 𝑏)
12		wemapsolem.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)
13		simprll 776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝑈)
14	1, 13	sselid 3920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑m 𝐴))
15		elmapi 8646	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (𝐵 ↑m 𝐴) → 𝑎:𝐴⟶𝐵)
16	14, 15	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵)
17	16	ffnd 6610	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴)
18		simprlr 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝑈)
19	1, 18	sselid 3920	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑m 𝐴))
20		elmapi 8646	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝐵 ↑m 𝐴) → 𝑏:𝐴⟶𝐵)
21	19, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵)
22	21	ffnd 6610	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴)
23		fndmdif 6928	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
24	17, 22, 23	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
25	24	eleq2d 2825	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
26		nesym 3001	. . . . . . . . . . . . . . 15 ⊢ ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑥) = (𝑎‘𝑥))
27		fveq2 6783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑏‘𝑥) = (𝑏‘𝑐))
28		fveq2 6783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑎‘𝑥) = (𝑎‘𝑐))
29	27, 28	eqeq12d 2755	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑐 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑐) = (𝑎‘𝑐)))
30	29	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑐 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
31	26, 30	bitrid 282	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑐 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
32	31	elrab 3625	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
33	25, 32	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐))))
34	24	eleq2d 2825	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
35		fveq2 6783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑏‘𝑥) = (𝑏‘𝑑))
36		fveq2 6783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑎‘𝑥) = (𝑎‘𝑑))
37	35, 36	eqeq12d 2755	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑑 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑑) = (𝑎‘𝑑)))
38	37	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑑 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
39	26, 38	bitrid 282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑑 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
40	39	elrab 3625	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
41	34, 40	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑))))
42	41	imbi1d 342	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐)))
43		impexp 451	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
44		con34b 316	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐))
45	44	imbi2i 336	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
46	43, 45	bitr4i 277	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
47	42, 46	bitrdi 287	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
48	47	ralbidv2 3111	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
49	33, 48	anbi12d 631	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
50		anass 469	. . . . . . . . . . 11 ⊢ (((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
51	49, 50	bitrdi 287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))))
52	51	rexbidv2 3225	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
53	12, 52	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
54	3	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑆 Or 𝐵)
55	21	ffvelrnda 6970	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑏‘𝑐) ∈ 𝐵)
56	16	ffvelrnda 6970	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑎‘𝑐) ∈ 𝐵)
57		sotrieq 5533	. . . . . . . . . . . . 13 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → ((𝑏‘𝑐) = (𝑎‘𝑐) ↔ ¬ ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
58	57	con2bid 355	. . . . . . . . . . . 12 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
59	58	biimprd 247	. . . . . . . . . . 11 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
60	54, 55, 56, 59	syl12anc 834	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
61	60	anim1d 611	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
62	61	reximdva 3204	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
63	53, 62	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
64	6	wemaplem1 9314	. . . . . . . . . 10 ⊢ ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
65	64	el2v 3441	. . . . . . . . 9 ⊢ (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
66	6	wemaplem1 9314	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
67	66	el2v 3441	. . . . . . . . 9 ⊢ (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
68	65, 67	orbi12i 912	. . . . . . . 8 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
69		r19.43 3281	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
70		andir 1006	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
71		eqcom 2746	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑑) = (𝑎‘𝑑) ↔ (𝑎‘𝑑) = (𝑏‘𝑑))
72	71	imbi2i 336	. . . . . . . . . . . . 13 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
73	72	ralbii 3093	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
74	73	anbi2i 623	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
75	74	orbi2i 910	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
76	70, 75	bitr2i 275	. . . . . . . . 9 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
77	76	rexbii 3182	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
78	68, 69, 77	3bitr2i 299	. . . . . . 7 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
79	63, 78	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
80	79	expr 457	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 ≠ 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
81	11, 80	syl5bir 242	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
82	81	orrd 860	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
83		3orrot 1091	. . . 4 ⊢ ((𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎) ↔ (𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
84		3orass 1089	. . . 4 ⊢ ((𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
85	83, 84	bitr2i 275	. . 3 ⊢ ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
86	82, 85	sylib 217	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
87	10, 86	issod 5537	1 ⊢ (𝜑 → 𝑇 Or 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∨ w3o 1085   = wceq 1539   ∈ wcel 2107   ≠ wne 2944  ∀wral 3065  ∃wrex 3066  {crab 3069  Vcvv 3433   ∖ cdif 3885   ⊆ wss 3888   class class class wbr 5075  {copab 5137   Po wpo 5502   Or wor 5503  dom cdm 5590   Fn wfn 6432  ⟶wf 6433  ‘cfv 6437  (class class class)co 7284   ↑_m cmap 8624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-1st 7840  df-2nd 7841  df-map 8626

This theorem is referenced by:  wemapso  9319  wemapso2lem  9320