Theorem dmopab3rexdif 33080

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

Assertion

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

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

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

Proof of Theorem dmopab3rexdif

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rexcom4 3172	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑦∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵))
2		rexcom4 3172	. . . . . . . . . 10 ⊢ (∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑦∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷))
3	1, 2	orbi12i 915	. . . . . . . . 9 ⊢ ((∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑦∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑦∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
4		19.43 1890	. . . . . . . . 9 ⊢ (∃𝑦(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑦∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑦∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
5	3, 4	bitr4i 281	. . . . . . . 8 ⊢ ((∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑦(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
6	5	rexbii 3170	. . . . . . 7 ⊢ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈 ∖ 𝑆)∃𝑦(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
7		rexcom4 3172	. . . . . . 7 ⊢ (∃𝑢 ∈ (𝑈 ∖ 𝑆)∃𝑦(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑦∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
8	6, 7	bitri 278	. . . . . 6 ⊢ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑦∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
9		rexcom4 3172	. . . . . . . 8 ⊢ (∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑦∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵))
10	9	rexbii 3170	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑢 ∈ 𝑆 ∃𝑦∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵))
11		rexcom4 3172	. . . . . . 7 ⊢ (∃𝑢 ∈ 𝑆 ∃𝑦∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑦∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵))
12	10, 11	bitri 278	. . . . . 6 ⊢ (∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑦∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵))
13	8, 12	orbi12i 915	. . . . 5 ⊢ ((∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)) ↔ (∃𝑦∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑦∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
14		19.43 1890	. . . . 5 ⊢ (∃𝑦(∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)) ↔ (∃𝑦∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑦∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
15	13, 14	bitr4i 281	. . . 4 ⊢ ((∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)) ↔ ∃𝑦(∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
16		difssd 4047	. . . . . . . 8 ⊢ (𝑆 ⊆ 𝑈 → (𝑈 ∖ 𝑆) ⊆ 𝑈)
17		ssralv 3967	. . . . . . . 8 ⊢ ((𝑈 ∖ 𝑆) ⊆ 𝑈 → (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ∀𝑢 ∈ (𝑈 ∖ 𝑆)(∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊)))
18	16, 17	syl 17	. . . . . . 7 ⊢ (𝑆 ⊆ 𝑈 → (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ∀𝑢 ∈ (𝑈 ∖ 𝑆)(∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊)))
19	18	impcom 411	. . . . . 6 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → ∀𝑢 ∈ (𝑈 ∖ 𝑆)(∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊))
20		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑧 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑧 = 𝐴)
21	20	exlimiv 1938	. . . . . . . . . . 11 ⊢ (∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) → 𝑧 = 𝐴)
22		elisset 2819	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑋 → ∃𝑦 𝑦 = 𝐵)
23		ibar 532	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐴 → (𝑦 = 𝐵 ↔ (𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
24	23	bicomd 226	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐴 → ((𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ 𝑦 = 𝐵))
25	24	exbidv 1929	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐴 → (∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑦 𝑦 = 𝐵))
26	22, 25	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑋 → (𝑧 = 𝐴 → ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
27	21, 26	impbid2 229	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑋 → (∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ 𝑧 = 𝐴))
28	27	ralrexbid 3241	. . . . . . . . 9 ⊢ (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 → (∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑣 ∈ 𝑈 𝑧 = 𝐴))
29	28	adantr 484	. . . . . . . 8 ⊢ ((∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑣 ∈ 𝑈 𝑧 = 𝐴))
30		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑧 = 𝐶 ∧ 𝑦 = 𝐷) → 𝑧 = 𝐶)
31	30	exlimiv 1938	. . . . . . . . . . 11 ⊢ (∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) → 𝑧 = 𝐶)
32		elisset 2819	. . . . . . . . . . . 12 ⊢ (𝐷 ∈ 𝑊 → ∃𝑦 𝑦 = 𝐷)
33		ibar 532	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝐶 → (𝑦 = 𝐷 ↔ (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
34	33	bicomd 226	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐶 → ((𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ 𝑦 = 𝐷))
35	34	exbidv 1929	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝐶 → (∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑦 𝑦 = 𝐷))
36	32, 35	syl5ibrcom 250	. . . . . . . . . . 11 ⊢ (𝐷 ∈ 𝑊 → (𝑧 = 𝐶 → ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
37	31, 36	impbid2 229	. . . . . . . . . 10 ⊢ (𝐷 ∈ 𝑊 → (∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ 𝑧 = 𝐶))
38	37	ralrexbid 3241	. . . . . . . . 9 ⊢ (∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 → (∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶))
39	38	adantl 485	. . . . . . . 8 ⊢ ((∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶))
40	29, 39	orbi12d 919	. . . . . . 7 ⊢ ((∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ((∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
41	40	ralrexbid 3241	. . . . . 6 ⊢ (∀𝑢 ∈ (𝑈 ∖ 𝑆)(∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
42	19, 41	syl 17	. . . . 5 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
43		ssralv 3967	. . . . . . . 8 ⊢ (𝑆 ⊆ 𝑈 → (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ∀𝑢 ∈ 𝑆 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊)))
44		ssralv 3967	. . . . . . . . . . 11 ⊢ ((𝑈 ∖ 𝑆) ⊆ 𝑈 → (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 → ∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋))
45	16, 44	syl 17	. . . . . . . . . 10 ⊢ (𝑆 ⊆ 𝑈 → (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 → ∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋))
46	45	adantrd 495	. . . . . . . . 9 ⊢ (𝑆 ⊆ 𝑈 → ((∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋))
47	46	ralimdv 3101	. . . . . . . 8 ⊢ (𝑆 ⊆ 𝑈 → (∀𝑢 ∈ 𝑆 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋))
48	43, 47	syld 47	. . . . . . 7 ⊢ (𝑆 ⊆ 𝑈 → (∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋))
49	48	impcom 411	. . . . . 6 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → ∀𝑢 ∈ 𝑆 ∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋)
50	27	ralrexbid 3241	. . . . . . 7 ⊢ (∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋 → (∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴))
51	50	ralrexbid 3241	. . . . . 6 ⊢ (∀𝑢 ∈ 𝑆 ∀𝑣 ∈ (𝑈 ∖ 𝑆)𝐵 ∈ 𝑋 → (∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴))
52	49, 51	syl 17	. . . . 5 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → (∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴))
53	42, 52	orbi12d 919	. . . 4 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → ((∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 ∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 ∃𝑦(𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)∃𝑦(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴)))
54	15, 53	bitr3id 288	. . 3 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → (∃𝑦(∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴)))
55		eqeq1 2741	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝐴 ↔ 𝑧 = 𝐴))
56	55	anbi1d 633	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
57	56	rexbidv 3216	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
58		eqeq1 2741	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑧 = 𝐶))
59	58	anbi1d 633	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
60	59	rexbidv 3216	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷) ↔ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)))
61	57, 60	orbi12d 919	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ (∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷))))
62	61	rexbidv 3216	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷))))
63	56	2rexbidv 3219	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
64	62, 63	orbi12d 919	. . . . 5 ⊢ (𝑥 = 𝑧 → ((∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵))))
65	64	dmopabelb 5785	. . . 4 ⊢ (𝑧 ∈ V → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))} ↔ ∃𝑦(∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵))))
66	65	elv 3414	. . 3 ⊢ (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))} ↔ ∃𝑦(∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑧 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑧 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑧 = 𝐴 ∧ 𝑦 = 𝐵)))
67		vex 3412	. . . 4 ⊢ 𝑧 ∈ V
68	55	rexbidv 3216	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ↔ ∃𝑣 ∈ 𝑈 𝑧 = 𝐴))
69	58	rexbidv 3216	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∃𝑖 ∈ 𝐼 𝑥 = 𝐶 ↔ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶))
70	68, 69	orbi12d 919	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ↔ (∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
71	70	rexbidv 3216	. . . . 5 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ↔ ∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶)))
72	55	2rexbidv 3219	. . . . 5 ⊢ (𝑥 = 𝑧 → (∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑥 = 𝐴 ↔ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴))
73	71, 72	orbi12d 919	. . . 4 ⊢ (𝑥 = 𝑧 → ((∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑥 = 𝐴) ↔ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴)))
74	67, 73	elab 3587	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑥 = 𝐴)} ↔ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑧 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑧 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑧 = 𝐴))
75	54, 66, 74	3bitr4g 317	. 2 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))} ↔ 𝑧 ∈ {𝑥 ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑥 = 𝐴)}))
76	75	eqrdv 2735	1 ⊢ ((∀𝑢 ∈ 𝑈 (∀𝑣 ∈ 𝑈 𝐵 ∈ 𝑋 ∧ ∀𝑖 ∈ 𝐼 𝐷 ∈ 𝑊) ∧ 𝑆 ⊆ 𝑈) → dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 (𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∨ ∃𝑖 ∈ 𝐼 (𝑥 = 𝐶 ∧ 𝑦 = 𝐷)) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)(𝑥 = 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ (∃𝑢 ∈ (𝑈 ∖ 𝑆)(∃𝑣 ∈ 𝑈 𝑥 = 𝐴 ∨ ∃𝑖 ∈ 𝐼 𝑥 = 𝐶) ∨ ∃𝑢 ∈ 𝑆 ∃𝑣 ∈ (𝑈 ∖ 𝑆)𝑥 = 𝐴)})

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 847   = wceq 1543  ∃wex 1787   ∈ wcel 2110  {cab 2714  ∀wral 3061  ∃wrex 3062  Vcvv 3408   ∖ cdif 3863   ⊆ wss 3866  {copab 5115  dom cdm 5551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-br 5054  df-opab 5116  df-dm 5561

This theorem is referenced by:  satffunlem2lem2  33081