or2expropbi

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)

		Ref	Expression
	Assertion	or2expropbi	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\exists a \exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)) \leftrightarrow \exists a \exists b (⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)))$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ a ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B))$
2		nfv	$⊢ Ⅎ a ⟨A, B⟩ = ⟨x, y⟩$
3		nfcv	$⊢ \underline{Ⅎ} a y$
4		nfsbc1v	$⊢ Ⅎ a \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ)$
5	3 4	nfsbcw	$⊢ Ⅎ a \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ)$
6	2 5	nfan	$⊢ Ⅎ a (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))$
7	6	nfex	$⊢ Ⅎ a \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))$
8	7	nfex	$⊢ Ⅎ a \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))$
9		nfv	$⊢ Ⅎ b ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B))$
10		nfv	$⊢ Ⅎ b ⟨A, B⟩ = ⟨x, y⟩$
11		nfsbc1v	$⊢ Ⅎ b \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ)$
12	10 11	nfan	$⊢ Ⅎ b (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))$
13	12	nfex	$⊢ Ⅎ b \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))$
14	13	nfex	$⊢ Ⅎ b \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))$
15		vex	$⊢ a \in V$
16		vex	$⊢ b \in V$
17		preq12bg	$⊢ ((A \in X \land B \in X) \land (a \in V \land b \in V)) \to (\{A, B\} = \{a, b\} \leftrightarrow ((A = a \land B = b) \lor (A = b \land B = a)))$
18	15 16 17	mpanr12	$⊢ (A \in X \land B \in X) \to (\{A, B\} = \{a, b\} \leftrightarrow ((A = a \land B = b) \lor (A = b \land B = a)))$
19	18	3adant3	$⊢ (A \in X \land B \in X \land A R B) \to (\{A, B\} = \{a, b\} \leftrightarrow ((A = a \land B = b) \lor (A = b \land B = a)))$
20	19	adantl	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\{A, B\} = \{a, b\} \leftrightarrow ((A = a \land B = b) \lor (A = b \land B = a)))$
21		or2expropbilem1	$⊢ (A \in X \land B \in X) \to ((A = a \land B = b) \to ((a R b \land φ) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
22	21	3adant3	$⊢ (A \in X \land B \in X \land A R B) \to ((A = a \land B = b) \to ((a R b \land φ) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
23	22	adantl	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to ((A = a \land B = b) \to ((a R b \land φ) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
24		breq12	$⊢ (B = a \land A = b) \to (B R A \leftrightarrow a R b)$
25	24	ancoms	$⊢ (A = b \land B = a) \to (B R A \leftrightarrow a R b)$
26	25	adantl	$⊢ (((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \land (A = b \land B = a)) \to (B R A \leftrightarrow a R b)$
27		soasym	$⊢ (R Or X \land (A \in X \land B \in X)) \to (A R B \to \neg B R A)$
28	27	ex	$⊢ R Or X \to ((A \in X \land B \in X) \to (A R B \to \neg B R A))$
29	28	adantl	$⊢ (X \in V \land R Or X) \to ((A \in X \land B \in X) \to (A R B \to \neg B R A))$
30	29	expd	$⊢ (X \in V \land R Or X) \to (A \in X \to (B \in X \to (A R B \to \neg B R A)))$
31	30	3imp2	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to \neg B R A$
32	31	pm2.21d	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (B R A \to (φ \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
33	32	adantr	$⊢ (((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \land (A = b \land B = a)) \to (B R A \to (φ \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
34	26 33	sylbird	$⊢ (((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \land (A = b \land B = a)) \to (a R b \to (φ \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
35	34	impd	$⊢ (((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \land (A = b \land B = a)) \to ((a R b \land φ) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ)))$
36	35	ex	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to ((A = b \land B = a) \to ((a R b \land φ) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
37	23 36	jaod	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (((A = a \land B = b) \lor (A = b \land B = a)) \to ((a R b \land φ) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
38	20 37	sylbid	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\{A, B\} = \{a, b\} \to ((a R b \land φ) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))))$
39	38	impd	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to ((\{A, B\} = \{a, b\} \land (a R b \land φ)) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ)))$
40	9 14 39	exlimd	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ)))$
41	1 8 40	exlimd	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\exists a \exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)) \to \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ)))$
42		or2expropbilem2	$⊢ \exists a \exists b (⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)) \leftrightarrow \exists x \exists y (⟨A, B⟩ = ⟨x, y⟩ \land \underset{˙}{[} y / b \underset{˙}{]} \underset{˙}{[} x / a \underset{˙}{]} (a R b \land φ))$
43	41 42	imbitrrdi	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\exists a \exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)) \to \exists a \exists b (⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)))$
44		oppr	$⊢ (A \in X \land B \in X) \to (⟨A, B⟩ = ⟨a, b⟩ \to \{A, B\} = \{a, b\})$
45	44	anim1d	$⊢ (A \in X \land B \in X) \to ((⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)) \to (\{A, B\} = \{a, b\} \land (a R b \land φ)))$
46	45	2eximdv	$⊢ (A \in X \land B \in X) \to (\exists a \exists b (⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)) \to \exists a \exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)))$
47	46	3adant3	$⊢ (A \in X \land B \in X \land A R B) \to (\exists a \exists b (⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)) \to \exists a \exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)))$
48	47	adantl	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\exists a \exists b (⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)) \to \exists a \exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)))$
49	43 48	impbid	$⊢ ((X \in V \land R Or X) \land (A \in X \land B \in X \land A R B)) \to (\exists a \exists b (\{A, B\} = \{a, b\} \land (a R b \land φ)) \leftrightarrow \exists a \exists b (⟨A, B⟩ = ⟨a, b⟩ \land (a R b \land φ)))$

Metamath Proof Explorer

Theorem or2expropbi

Proof