Theorem or2expropbi 47626

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 1937	. . . 4 ⊢ Ⅎ𝑎((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵))
2		nfv 1937	. . . . . . 7 ⊢ Ⅎ𝑎⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩
3		nfcv 2927	. . . . . . . 8 ⊢ Ⅎ𝑎𝑦
4		nfsbc1v 3767	. . . . . . . 8 ⊢ Ⅎ𝑎[𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)
5	3, 4	nfsbcw 3769	. . . . . . 7 ⊢ Ⅎ𝑎[𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)
6	2, 5	nfan 1922	. . . . . 6 ⊢ Ⅎ𝑎(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
7	6	nfex 2359	. . . . 5 ⊢ Ⅎ𝑎∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
8	7	nfex 2359	. . . 4 ⊢ Ⅎ𝑎∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
9		nfv 1937	. . . . 5 ⊢ Ⅎ𝑏((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵))
10		nfv 1937	. . . . . . . 8 ⊢ Ⅎ𝑏⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩
11		nfsbc1v 3767	. . . . . . . 8 ⊢ Ⅎ𝑏[𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)
12	10, 11	nfan 1922	. . . . . . 7 ⊢ Ⅎ𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
13	12	nfex 2359	. . . . . 6 ⊢ Ⅎ𝑏∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
14	13	nfex 2359	. . . . 5 ⊢ Ⅎ𝑏∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))
15		vex 3461	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
16		vex 3461	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
17		preq12bg 4814	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝑎 ∈ V ∧ 𝑏 ∈ V)) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
18	15, 16, 17	mpanr12 717	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
19	18	3adant3 1148	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
20	19	adantl 486	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ({𝐴, 𝐵} = {𝑎, 𝑏} ↔ ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎))))
21		or2expropbilem1 47624	. . . . . . . . . 10 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
22	21	3adant3 1148	. . . . . . . . 9 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
23	22	adantl 486	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
24		breq12 5110	. . . . . . . . . . . . 13 ⊢ ((𝐵 = 𝑎 ∧ 𝐴 = 𝑏) → (𝐵𝑅𝐴 ↔ 𝑎𝑅𝑏))
25	24	ancoms 463	. . . . . . . . . . . 12 ⊢ ((𝐴 = 𝑏 ∧ 𝐵 = 𝑎) → (𝐵𝑅𝐴 ↔ 𝑎𝑅𝑏))
26	25	adantl 486	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → (𝐵𝑅𝐴 ↔ 𝑎𝑅𝑏))
27		soasym 5593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 Or 𝑋 ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴))
28	27	ex 417	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Or 𝑋 → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴)))
29	28	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴)))
30	29	expd 420	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) → (𝐴 ∈ 𝑋 → (𝐵 ∈ 𝑋 → (𝐴𝑅𝐵 → ¬ 𝐵𝑅𝐴))))
31	30	3imp2 1366	. . . . . . . . . . . . 13 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ¬ 𝐵𝑅𝐴)
32	31	pm2.21d 122	. . . . . . . . . . . 12 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (𝐵𝑅𝐴 → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
33	32	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → (𝐵𝑅𝐴 → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
34	26, 33	sylbird 263	. . . . . . . . . 10 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → (𝑎𝑅𝑏 → (𝜑 → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
35	34	impd 415	. . . . . . . . 9 ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) ∧ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
36	35	ex 417	. . . . . . . 8 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ((𝐴 = 𝑏 ∧ 𝐵 = 𝑎) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
37	23, 36	jaod 872	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (((𝐴 = 𝑎 ∧ 𝐵 = 𝑏) ∨ (𝐴 = 𝑏 ∧ 𝐵 = 𝑎)) → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
38	20, 37	sylbid 243	. . . . . 6 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → ({𝐴, 𝐵} = {𝑎, 𝑏} → ((𝑎𝑅𝑏 ∧ 𝜑) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))))
39	38	impd 415	. . . . 5 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
40	9, 14, 39	exlimd 2256	. . . 4 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
41	1, 8, 40	exlimd 2256	. . 3 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑))))
42		or2expropbilem2 47625	. . 3 ⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑥∃𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑦 / 𝑏][𝑥 / 𝑎](𝑎𝑅𝑏 ∧ 𝜑)))
43	41, 42	imbitrrdi 255	. 2 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
44		oppr 47622	. . . . . 6 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ → {𝐴, 𝐵} = {𝑎, 𝑏}))
45	44	anim1d 622	. . . . 5 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
46	45	2eximdv 1942	. . . 4 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
47	46	3adant3 1148	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵) → (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
48	47	adantl 486	. 2 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑)) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑))))
49	43, 48	impbid 215	1 ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑅 Or 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐴𝑅𝐵)) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ (𝑎𝑅𝑏 ∧ 𝜑)) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ (𝑎𝑅𝑏 ∧ 𝜑))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145  Vcvv 3457  [wsbc 3747  {cpr 4587  ⟨cop 4591   class class class wbr 5105   Or wor 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-po 5560  df-so 5561

This theorem is referenced by: (None)