Theorem wemapsolem 9486

Description: Lemma for wemapso 9487. (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 5564	. . . . 5 ⊢ (𝑆 Or 𝐵 → 𝑆 Po 𝐵)
5	3, 4	syl 17	. . . 4 ⊢ (𝜑 → 𝑆 Po 𝐵)
6		wemapso.t	. . . . 5 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
7	6	wemappo 9485	. . . 4 ⊢ ((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐵 ↑m 𝐴))
8	2, 5, 7	syl2anc 584	. . 3 ⊢ (𝜑 → 𝑇 Po (𝐵 ↑m 𝐴))
9		poss 5547	. . 3 ⊢ (𝑈 ⊆ (𝐵 ↑m 𝐴) → (𝑇 Po (𝐵 ↑m 𝐴) → 𝑇 Po 𝑈))
10	1, 8, 9	mpsyl 68	. 2 ⊢ (𝜑 → 𝑇 Po 𝑈)
11		df-ne 2944	. . . . 5 ⊢ (𝑎 ≠ 𝑏 ↔ ¬ 𝑎 = 𝑏)
12		wemapsolem.4	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐)
13		simprll 777	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 𝑈)
14	1, 13	sselid 3942	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ (𝐵 ↑m 𝐴))
15		elmapi 8787	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (𝐵 ↑m 𝐴) → 𝑎:𝐴⟶𝐵)
16	14, 15	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎:𝐴⟶𝐵)
17	16	ffnd 6669	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑎 Fn 𝐴)
18		simprlr 778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 𝑈)
19	1, 18	sselid 3942	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ (𝐵 ↑m 𝐴))
20		elmapi 8787	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ (𝐵 ↑m 𝐴) → 𝑏:𝐴⟶𝐵)
21	19, 20	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏:𝐴⟶𝐵)
22	21	ffnd 6669	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → 𝑏 Fn 𝐴)
23		fndmdif 6992	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
24	17, 22, 23	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → dom (𝑎 ∖ 𝑏) = {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)})
25	24	eleq2d 2823	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
26		nesym 3000	. . . . . . . . . . . . . . 15 ⊢ ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑥) = (𝑎‘𝑥))
27		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑏‘𝑥) = (𝑏‘𝑐))
28		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑐 → (𝑎‘𝑥) = (𝑎‘𝑐))
29	27, 28	eqeq12d 2752	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑐 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑐) = (𝑎‘𝑐)))
30	29	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑐 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
31	26, 30	bitrid 282	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑐 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
32	31	elrab 3645	. . . . . . . . . . . . 13 ⊢ (𝑐 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
33	25, 32	bitrdi 286	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑐 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐))))
34	24	eleq2d 2823	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ 𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)}))
35		fveq2 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑏‘𝑥) = (𝑏‘𝑑))
36		fveq2 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑑 → (𝑎‘𝑥) = (𝑎‘𝑑))
37	35, 36	eqeq12d 2752	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑑 → ((𝑏‘𝑥) = (𝑎‘𝑥) ↔ (𝑏‘𝑑) = (𝑎‘𝑑)))
38	37	notbid 317	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑑 → (¬ (𝑏‘𝑥) = (𝑎‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
39	26, 38	bitrid 282	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑑 → ((𝑎‘𝑥) ≠ (𝑏‘𝑥) ↔ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
40	39	elrab 3645	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ {𝑥 ∈ 𝐴 ∣ (𝑎‘𝑥) ≠ (𝑏‘𝑥)} ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)))
41	34, 40	bitrdi 286	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑑 ∈ dom (𝑎 ∖ 𝑏) ↔ (𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑))))
42	41	imbi1d 341	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ ((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐)))
43		impexp 451	. . . . . . . . . . . . . . 15 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
44		con34b 315	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐))
45	44	imbi2i 335	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑑 ∈ 𝐴 → (¬ (𝑏‘𝑑) = (𝑎‘𝑑) → ¬ 𝑑𝑅𝑐)))
46	43, 45	bitr4i 277	. . . . . . . . . . . . . 14 ⊢ (((𝑑 ∈ 𝐴 ∧ ¬ (𝑏‘𝑑) = (𝑎‘𝑑)) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
47	42, 46	bitrdi 286	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑑 ∈ dom (𝑎 ∖ 𝑏) → ¬ 𝑑𝑅𝑐) ↔ (𝑑 ∈ 𝐴 → (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
48	47	ralbidv2 3170	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
49	33, 48	anbi12d 631	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ ((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
50		anass 469	. . . . . . . . . . 11 ⊢ (((𝑐 ∈ 𝐴 ∧ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
51	49, 50	bitrdi 286	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ((𝑐 ∈ dom (𝑎 ∖ 𝑏) ∧ ∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐) ↔ (𝑐 ∈ 𝐴 ∧ (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))))
52	51	rexbidv2 3171	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ dom (𝑎 ∖ 𝑏)∀𝑑 ∈ dom (𝑎 ∖ 𝑏) ¬ 𝑑𝑅𝑐 ↔ ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
53	12, 52	mpbid 231	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
54	3	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → 𝑆 Or 𝐵)
55	21	ffvelcdmda 7035	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑏‘𝑐) ∈ 𝐵)
56	16	ffvelcdmda 7035	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (𝑎‘𝑐) ∈ 𝐵)
57		sotrieq 5574	. . . . . . . . . . . . 13 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → ((𝑏‘𝑐) = (𝑎‘𝑐) ↔ ¬ ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
58	57	con2bid 354	. . . . . . . . . . . 12 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ↔ ¬ (𝑏‘𝑐) = (𝑎‘𝑐)))
59	58	biimprd 247	. . . . . . . . . . 11 ⊢ ((𝑆 Or 𝐵 ∧ ((𝑏‘𝑐) ∈ 𝐵 ∧ (𝑎‘𝑐) ∈ 𝐵)) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
60	54, 55, 56, 59	syl12anc 835	. . . . . . . . . 10 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → (¬ (𝑏‘𝑐) = (𝑎‘𝑐) → ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐))))
61	60	anim1d 611	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) ∧ 𝑐 ∈ 𝐴) → ((¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
62	61	reximdva 3165	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (∃𝑐 ∈ 𝐴 (¬ (𝑏‘𝑐) = (𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
63	53, 62	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
64	6	wemaplem1 9482	. . . . . . . . . 10 ⊢ ((𝑏 ∈ V ∧ 𝑎 ∈ V) → (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
65	64	el2v 3453	. . . . . . . . 9 ⊢ (𝑏𝑇𝑎 ↔ ∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
66	6	wemaplem1 9482	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V) → (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
67	66	el2v 3453	. . . . . . . . 9 ⊢ (𝑎𝑇𝑏 ↔ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
68	65, 67	orbi12i 913	. . . . . . . 8 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
69		r19.43 3125	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (∃𝑐 ∈ 𝐴 ((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ∃𝑐 ∈ 𝐴 ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
70		andir 1007	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))))
71		eqcom 2743	. . . . . . . . . . . . . 14 ⊢ ((𝑏‘𝑑) = (𝑎‘𝑑) ↔ (𝑎‘𝑑) = (𝑏‘𝑑))
72	71	imbi2i 335	. . . . . . . . . . . . 13 ⊢ ((𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
73	72	ralbii 3096	. . . . . . . . . . . 12 ⊢ (∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)) ↔ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))
74	73	anbi2i 623	. . . . . . . . . . 11 ⊢ (((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ↔ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑))))
75	74	orbi2i 911	. . . . . . . . . 10 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))))
76	70, 75	bitr2i 275	. . . . . . . . 9 ⊢ ((((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
77	76	rexbii 3097	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))) ∨ ((𝑎‘𝑐)𝑆(𝑏‘𝑐) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑎‘𝑑) = (𝑏‘𝑑)))) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
78	68, 69, 77	3bitr2i 298	. . . . . . 7 ⊢ ((𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ ∃𝑐 ∈ 𝐴 (((𝑏‘𝑐)𝑆(𝑎‘𝑐) ∨ (𝑎‘𝑐)𝑆(𝑏‘𝑐)) ∧ ∀𝑑 ∈ 𝐴 (𝑑𝑅𝑐 → (𝑏‘𝑑) = (𝑎‘𝑑))))
79	63, 78	sylibr 233	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈) ∧ 𝑎 ≠ 𝑏)) → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
80	79	expr 457	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 ≠ 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
81	11, 80	biimtrrid 242	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (¬ 𝑎 = 𝑏 → (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
82	81	orrd 861	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
83		3orrot 1092	. . . 4 ⊢ ((𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎) ↔ (𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏))
84		3orass 1090	. . . 4 ⊢ ((𝑎 = 𝑏 ∨ 𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏) ↔ (𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)))
85	83, 84	bitr2i 275	. . 3 ⊢ ((𝑎 = 𝑏 ∨ (𝑏𝑇𝑎 ∨ 𝑎𝑇𝑏)) ↔ (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
86	82, 85	sylib 217	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ 𝑏 ∈ 𝑈)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎))
87	10, 86	issod 5578	1 ⊢ (𝜑 → 𝑇 Or 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∖ cdif 3907   ⊆ wss 3910   class class class wbr 5105  {copab 5167   Po wpo 5543   Or wor 5544  dom cdm 5633   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357   ↑_m cmap 8765

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 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767

This theorem is referenced by:  wemapso  9487  wemapso2lem  9488