Theorem or2expropbi 46478

Description: If two classes are strictly ordered, there is an ordered pair of both classes fulfilling a wff iff there is an unordered pair of both classes fulfilling the wff. (Contributed by AV, 26-Aug-2023.)

Assertion

Ref	Expression
or2expropbi	⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))

Distinct variable groups:   𝑎,𝑏,𝐴   𝐵,𝑎,𝑏   𝑅,𝑎,𝑏   𝑉,𝑎,𝑏   𝑋,𝑎,𝑏

Allowed substitution hints:   𝜑(𝑎,𝑏)

Proof of Theorem or2expropbi

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1909	. . . 4 ⊢ Ⅎ𝑎((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵))
2		nfv 1909	. . . . . . 7 ⊢ Ⅎ𝑎⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩
3		nfcv 2892	. . . . . . . 8 ⊢ Ⅎ𝑎𝑦
4		nfsbc1v 3789	. . . . . . . 8 ⊢ Ⅎ𝑎[𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)
5	3, 4	nfsbcw 3791	. . . . . . 7 ⊢ Ⅎ𝑎[𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)
6	2, 5	nfan 1894	. . . . . 6 ⊢ Ⅎ𝑎(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
7	6	nfex 2312	. . . . 5 ⊢ Ⅎ𝑎∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
8	7	nfex 2312	. . . 4 ⊢ Ⅎ𝑎∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
9		nfv 1909	. . . . 5 ⊢ Ⅎ𝑏((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵))
10		nfv 1909	. . . . . . . 8 ⊢ Ⅎ𝑏⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩
11		nfsbc1v 3789	. . . . . . . 8 ⊢ Ⅎ𝑏[𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)
12	10, 11	nfan 1894	. . . . . . 7 ⊢ Ⅎ𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
13	12	nfex 2312	. . . . . 6 ⊢ Ⅎ𝑏∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
14	13	nfex 2312	. . . . 5 ⊢ Ⅎ𝑏∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
15		vex 3467	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
16		vex 3467	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
17		preq12bg 4850	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
18	15, 16, 17	mpanr12 703	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
19	18	3adant3 1129	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
20	19	adantl 480	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
21		or2expropbilem1 46476	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
22	21	3adant3 1129	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
23	22	adantl 480	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
24		breq12 5148	. . . . . . . . . . . . 13 ⊢ ((𝐵 = 𝑎 ∧ 𝐴 = 𝑏) → (𝐵𝑅𝐴 ↔ 𝑎𝑅𝑏))
25	24	ancoms 457	. . . . . . . . . . . 12 ⊢ ((𝐴 = 𝑏 ∧ 𝐵 = 𝑎) → (𝐵𝑅𝐴 ↔ 𝑎𝑅𝑏))
26	25	adantl 480	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → (𝐵𝑅𝐴 ↔ 𝑎𝑅𝑏))
27		soasym 5615	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴))
28	27	ex 411	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Or 𝑋 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴)))
29	28	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴)))
30	29	expd 414	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) → (𝐴 ∈ 𝑋 → (𝐵 ∈ 𝑋 → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴))))
31	30	3imp2 1346	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ¬ 𝐵𝑅𝐴)
32	31	pm2.21d 121	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (𝐵𝑅𝐴 → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
33	32	adantr 479	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → (𝐵𝑅𝐴 → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
34	26, 33	sylbird 259	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → (𝑎𝑅𝑏 → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
35	34	impd 409	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
36	35	ex 411	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ((𝐴 = 𝑏 ∧ 𝐵 = 𝑎) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
37	23, 36	jaod 857	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
38	20, 37	sylbid 239	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ({𝐴, 𝐵} = {𝑎, 𝑏} → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
39	38	impd 409	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
40	9, 14, 39	exlimd 2206	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
41	1, 8, 40	exlimd 2206	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
42		or2expropbilem2 46477	. . 3 ⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))
43	41, 42	imbitrrdi 251	. 2 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
44		oppr 46474	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ → {𝐴, 𝐵} = {𝑎, 𝑏}))
45	44	anim1d 609	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
46	45	2eximdv 1914	. . . 4 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
47	46	3adant3 1129	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵) → (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
48	47	adantl 480	. 2 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
49	43, 48	impbid 211	1 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 845   ∧ w3a 1084   = wceq 1533  ∃wex 1773   ∈ wcel 2098  Vcvv 3463  [wsbc 3769  {cpr 4626  ⟨cop 4630   class class class wbr 5143   Or wor 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5294  ax-nul 5301  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3052  df-rab 3420  df-v 3465  df-sbc 3770  df-dif 3943  df-un 3945  df-ss 3957  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5144  df-po 5584  df-so 5585

This theorem is referenced by: (None)