Theorem wemapsolem 9526

Description: Lemma for wemapso 9527. (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 5586	. . . . 5 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
5	3, 4	syl 18	. . . 4 ⊢ (𝜑 → 𝑆 Po 𝐵)
6		wemapso.t	. . . . 5 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
7	6	wemappo 9525	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴))
8	2, 5, 7	syl2anc 596	. . 3 ⊢ (𝜑 → 𝑇 Po (𝐵 ↑m 𝐴))
9		poss 5569	. . 3 ⊢ (𝑈 ⊆ (𝐵 ↑m 𝐴) → (𝑇 Po (𝐵 ↑m 𝐴) → 𝑇 Po 𝑈))
10	1, 8, 9	mpsyl 69	. 2 ⊢ (𝜑 → 𝑇 Po 𝑈)
11		df-ne 2958	. . . . 5 ⊢ (𝑎 ≠ 𝑏 ↔ ¬ 𝑎 = 𝑏)
12		wemapsolem.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)
13		simprll 791	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝑈)
14	1, 13	sselid 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑m 𝐴))
15		elmapi 8852	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (𝐵 ↑m 𝐴) → 𝑎:𝐴⟶𝐵)
16	14, 15	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵)
17	16	ffnd 6707	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴)
18		simprlr 792	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝑈)
19	1, 18	sselid 3932	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑m 𝐴))
20		elmapi 8852	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝐵 ↑m 𝐴) → 𝑏:𝐴⟶𝐵)
21	19, 20	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵)
22	21	ffnd 6707	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴)
23		fndmdif 7038	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
24	17, 22, 23	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
25	24	eleq2d 2848	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
26		nesym 3013	. . . . . . . . . . . . . . 15 ⊢ ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑥) = (𝑎‘𝑥))
27		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑏‘𝑥) = (𝑏‘𝑐))
28		fveq2 6882	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑎‘𝑥) = (𝑎‘𝑐))
29	27, 28	eqeq12d 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑐 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑐) = (𝑎‘𝑐)))
30	29	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑐 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
31	26, 30	bitrid 286	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑐 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
32	31	elrab 3648	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
33	25, 32	bitrdi 290	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐))))
34	24	eleq2d 2848	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
35		fveq2 6882	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑏‘𝑥) = (𝑏‘𝑑))
36		fveq2 6882	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑎‘𝑥) = (𝑎‘𝑑))
37	35, 36	eqeq12d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑑 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑑) = (𝑎‘𝑑)))
38	37	notbid 321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑑 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
39	26, 38	bitrid 286	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑑 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
40	39	elrab 3648	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
41	34, 40	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑))))
42	41	imbi1d 344	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐)))
43		impexp 456	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
44		con34b 319	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐))
45	44	imbi2i 339	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
46	43, 45	bitr4i 281	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
47	42, 46	bitrdi 290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
48	47	ralbidv2 3183	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
49	33, 48	anbi12d 644	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
50		anass 474	. . . . . . . . . . 11 ⊢ (((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
51	49, 50	bitrdi 290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))))
52	51	rexbidv2 3184	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
53	12, 52	mpbid 235	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
54	3	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑆 Or 𝐵)
55	21	ffvelcdmda 7081	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑏‘𝑐) ∈ 𝐵)
56	16	ffvelcdmda 7081	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑎‘𝑐) ∈ 𝐵)
57		sotrieq 5598	. . . . . . . . . . . . 13 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → ((𝑏‘𝑐) = (𝑎‘𝑐) ↔ ¬ ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
58	57	con2bid 357	. . . . . . . . . . . 12 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
59	58	biimprd 251	. . . . . . . . . . 11 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
60	54, 55, 56, 59	syl12anc 850	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
61	60	anim1d 623	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
62	61	reximdva 3177	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
63	53, 62	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
64	6	wemaplem1 9522	. . . . . . . . . 10 ⊢ ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
65	64	el2v 3460	. . . . . . . . 9 ⊢ (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
66	6	wemaplem1 9522	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
67	66	el2v 3460	. . . . . . . . 9 ⊢ (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
68	65, 67	orbi12i 928	. . . . . . . 8 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
69		r19.43 3132	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
70		andir 1026	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
71		eqcom 2769	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑑) = (𝑎‘𝑑) ↔ (𝑎‘𝑑) = (𝑏‘𝑑))
72	71	imbi2i 339	. . . . . . . . . . . . 13 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
73	72	ralbii 3110	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
74	73	anbi2i 635	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
75	74	orbi2i 926	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
76	70, 75	bitr2i 279	. . . . . . . . 9 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
77	76	rexbii 3111	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
78	68, 69, 77	3bitr2i 302	. . . . . . 7 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
79	63, 78	sylibr 237	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
80	79	expr 462	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 ≠ 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
81	11, 80	biimtrrid 246	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
82	81	orrd 877	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
83		3orrot 1108	. . . 4 ⊢ ((𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎) ↔ (𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
84		3orass 1106	. . . 4 ⊢ ((𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
85	83, 84	bitr2i 279	. . 3 ⊢ ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
86	82, 85	sylib 221	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
87	10, 86	issod 5602	1 ⊢ (𝜑 → 𝑇 Or 𝑈)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  ∃wrex 3088  {crab 3414  Vcvv 3453   ∖ cdif 3899   ⊆ wss 3902   class class class wbr 5107  {copab 5171   Po wpo 5565   Or wor 5566  dom cdm 5659   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537  (class class class)co 7417   ↑_m cmap 8830

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-po 5567  df-so 5568  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7420  df-oprab 7421  df-mpo 7422  df-1st 7990  df-2nd 7991  df-map 8832

This theorem is used by:  wemapso  9527  wemapso2lem  9528