Theorem dmopab2rex 5786

Description: The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023.)

Assertion

Ref	Expression
dmopab2rex	⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)})

Distinct variable groups:   𝑥,𝐴,𝑦   𝐵,𝑖,𝑥,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐼,𝑦   𝑈,𝑖,𝑥,𝑦   𝑖,𝑉,𝑥,𝑦   𝑖,𝑋   𝑢,𝑖,𝑥,𝑦   𝑣,𝑖,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑣,𝑢,𝑖)   𝐵(𝑣,𝑢)   𝐶(𝑣,𝑢,𝑖)   𝐷(𝑣,𝑢,𝑖)   𝑈(𝑣,𝑢)   𝐼(𝑣,𝑢,𝑖)   𝑉(𝑣,𝑢)   𝑊(𝑥,𝑦,𝑣,𝑢,𝑖)   𝑋(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem dmopab2rex

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexcom4 3249	. . . . . . . 8 ⊢ (∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑦∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵))
2		rexcom4 3249	. . . . . . . 8 ⊢ (∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑦∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷))
3	1, 2	orbi12i 911	. . . . . . 7 ⊢ ((∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑦∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑦∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
4		19.43 1883	. . . . . . 7 ⊢ (∃𝑦(∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑦∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑦∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
5	3, 4	bitr4i 280	. . . . . 6 ⊢ ((∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑦(∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
6	5	rexbii 3247	. . . . 5 ⊢ (∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ 𝑈 ∃𝑦(∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
7		rexcom4 3249	. . . . 5 ⊢ (∃𝑢 ∈ 𝑈 ∃𝑦(∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑦∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
8	6, 7	bitri 277	. . . 4 ⊢ (∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑦∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
9		simpl 485	. . . . . . . . . 10 ⊢ ((𝑧 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑧 = 𝐴)
10	9	exlimiv 1931	. . . . . . . . 9 ⊢ (∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑧 = 𝐴)
11		elisset 3505	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑋 → ∃𝑦 𝑦 = 𝐵)
12		ibar 531	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (𝑦 = 𝐵 ↔ (𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
13	12	bicomd 225	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐴 → ((𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ 𝑦 = 𝐵))
14	13	exbidv 1922	. . . . . . . . . 10 ⊢ (𝑧 = 𝐴 → (∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑦 𝑦 = 𝐵))
15	11, 14	syl5ibrcom 249	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑋 → (𝑧 = 𝐴 → ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
16	10, 15	impbid2 228	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑋 → (∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ 𝑧 = 𝐴))
17	16	ralrexbid 3322	. . . . . . 7 ⊢ (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 → (∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑣 ∈ 𝑉 𝑧 = 𝐴))
18	17	adantr 483	. . . . . 6 ⊢ ((∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑣 ∈ 𝑉 𝑧 = 𝐴))
19		simpl 485	. . . . . . . . . 10 ⊢ ((𝑧 = 𝐶 ∧ 𝑦 = 𝐷) → 𝑧 = 𝐶)
20	19	exlimiv 1931	. . . . . . . . 9 ⊢ (∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) → 𝑧 = 𝐶)
21		elisset 3505	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑊 → ∃𝑦 𝑦 = 𝐷)
22		ibar 531	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐶 → (𝑦 = 𝐷 ↔ (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
23	22	bicomd 225	. . . . . . . . . . 11 ⊢ (𝑧 = 𝐶 → ((𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ 𝑦 = 𝐷))
24	23	exbidv 1922	. . . . . . . . . 10 ⊢ (𝑧 = 𝐶 → (∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑦 𝑦 = 𝐷))
25	21, 24	syl5ibrcom 249	. . . . . . . . 9 ⊢ (𝐷 ∈ 𝑊 → (𝑧 = 𝐶 → ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
26	20, 25	impbid2 228	. . . . . . . 8 ⊢ (𝐷 ∈ 𝑊 → (∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ 𝑧 = 𝐶))
27	26	ralrexbid 3322	. . . . . . 7 ⊢ (∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 → (∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶))
28	27	adantl 484	. . . . . 6 ⊢ ((∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶))
29	18, 28	orbi12d 915	. . . . 5 ⊢ ((∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ((∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
30	29	ralrexbid 3322	. . . 4 ⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
31	8, 30	syl5bbr 287	. . 3 ⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (∃𝑦∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
32		eqeq1 2825	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝐴 ↔ 𝑧 = 𝐴))
33	32	anbi1d 631	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
34	33	rexbidv 3297	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
35		eqeq1 2825	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑧 = 𝐶))
36	35	anbi1d 631	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → ((𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
37	36	rexbidv 3297	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
38	34, 37	orbi12d 915	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷))))
39	38	rexbidv 3297	. . . . 5 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷))))
40	39	dmopabelb 5785	. . . 4 ⊢ (𝑧 ∈ V → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} ↔ ∃𝑦∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷))))
41	40	elv 3499	. . 3 ⊢ (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} ↔ ∃𝑦∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
42		vex 3497	. . . 4 ⊢ 𝑧 ∈ V
43	32	rexbidv 3297	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ↔ ∃𝑣 ∈ 𝑉 𝑧 = 𝐴))
44	35	rexbidv 3297	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∃𝑖 ∈ 𝐼 𝑥 = 𝐶 ↔ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶))
45	43, 44	orbi12d 915	. . . . 5 ⊢ (𝑥 = 𝑧 → ((∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ↔ (∃𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
46	45	rexbidv 3297	. . . 4 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ↔ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
47	42, 46	elab 3667	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)} ↔ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶))
48	31, 41, 47	3bitr4g 316	. 2 ⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} ↔ 𝑧 ∈ {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)}))
49	48	eqrdv 2819	1 ⊢ (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢 ∈ 𝑈 (∃𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶)})

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2799  ∀wral 3138  ∃wrex 3139  Vcvv 3494  {copab 5128  dom cdm 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-dm 5565

This theorem is referenced by:  satffunlem1lem2  32650