Theorem ovmpt2df 5555

Description: Alternate deduction version of ovmpt2 5559, suitable for iteration. (Contributed by Mario Carneiro, 7-Jan-2017.)

Hypotheses

Ref	Expression
ovmpt2df.1	⊢ (φ → A ∈ 𝐶)
ovmpt2df.2	⊢ ((φ ∧ x = A) → B ∈ 𝐷)
ovmpt2df.3	⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 ∈ 𝑉)
ovmpt2df.4	⊢ ((φ ∧ (x = A ∧ y = B)) → ((A𝐹B) = 𝑅 → ψ))
ovmpt2df.5	⊢ Ⅎx𝐹
ovmpt2df.6	⊢ Ⅎxψ
ovmpt2df.7	⊢ Ⅎy𝐹
ovmpt2df.8	⊢ Ⅎyψ

Assertion

Ref	Expression
ovmpt2df	⊢ (φ → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))

Distinct variable groups:   x,y,A   y,B   φ,x,y

Allowed substitution hints:   ψ(x,y)   B(x)   𝐶(x,y)   𝐷(x,y)   𝑅(x,y)   𝐹(x,y)   𝑉(x,y)

Proof of Theorem ovmpt2df

Step	Hyp	Ref	Expression
1		nfv 1402	. 2 ⊢ Ⅎxφ
2		ovmpt2df.5	. . . 4 ⊢ Ⅎx𝐹
3		nfmpt21 5494	. . . 4 ⊢ Ⅎx(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
4	2, 3	nfeq 2167	. . 3 ⊢ Ⅎx 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
5		ovmpt2df.6	. . 3 ⊢ Ⅎxψ
6	4, 5	nfim 1446	. 2 ⊢ Ⅎx(𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)
7		ovmpt2df.1	. . . 4 ⊢ (φ → A ∈ 𝐶)
8		elex 2543	. . . 4 ⊢ (A ∈ 𝐶 → A ∈ V)
9	7, 8	syl 14	. . 3 ⊢ (φ → A ∈ V)
10		isset 2539	. . 3 ⊢ (A ∈ V ↔ ∃x x = A)
11	9, 10	sylib 127	. 2 ⊢ (φ → ∃x x = A)
12		ovmpt2df.2	. . . . 5 ⊢ ((φ ∧ x = A) → B ∈ 𝐷)
13		elex 2543	. . . . 5 ⊢ (B ∈ 𝐷 → B ∈ V)
14	12, 13	syl 14	. . . 4 ⊢ ((φ ∧ x = A) → B ∈ V)
15		isset 2539	. . . 4 ⊢ (B ∈ V ↔ ∃y y = B)
16	14, 15	sylib 127	. . 3 ⊢ ((φ ∧ x = A) → ∃y y = B)
17		nfv 1402	. . . 4 ⊢ Ⅎy(φ ∧ x = A)
18		ovmpt2df.7	. . . . . 6 ⊢ Ⅎy𝐹
19		nfmpt22 5495	. . . . . 6 ⊢ Ⅎy(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
20	18, 19	nfeq 2167	. . . . 5 ⊢ Ⅎy 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
21		ovmpt2df.8	. . . . 5 ⊢ Ⅎyψ
22	20, 21	nfim 1446	. . . 4 ⊢ Ⅎy(𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)
23		oveq 5442	. . . . . 6 ⊢ (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → (A𝐹B) = (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B))
24		simprl 471	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → x = A)
25		simprr 472	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → y = B)
26	24, 25	oveq12d 5454	. . . . . . . . 9 ⊢ ((φ ∧ (x = A ∧ y = B)) → (x(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)y) = (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B))
27	7	adantr 261	. . . . . . . . . . 11 ⊢ ((φ ∧ (x = A ∧ y = B)) → A ∈ 𝐶)
28	24, 27	eqeltrd 2096	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → x ∈ 𝐶)
29	12	adantrr 451	. . . . . . . . . . 11 ⊢ ((φ ∧ (x = A ∧ y = B)) → B ∈ 𝐷)
30	25, 29	eqeltrd 2096	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → y ∈ 𝐷)
31		ovmpt2df.3	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 ∈ 𝑉)
32		eqid 2022	. . . . . . . . . . 11 ⊢ (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
33	32	ovmpt4g 5546	. . . . . . . . . 10 ⊢ ((x ∈ 𝐶 ∧ y ∈ 𝐷 ∧ 𝑅 ∈ 𝑉) → (x(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)y) = 𝑅)
34	28, 30, 31, 33	syl3anc 1121	. . . . . . . . 9 ⊢ ((φ ∧ (x = A ∧ y = B)) → (x(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)y) = 𝑅)
35	26, 34	eqtr3d 2056	. . . . . . . 8 ⊢ ((φ ∧ (x = A ∧ y = B)) → (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B) = 𝑅)
36	35	eqeq2d 2033	. . . . . . 7 ⊢ ((φ ∧ (x = A ∧ y = B)) → ((A𝐹B) = (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B) ↔ (A𝐹B) = 𝑅))
37		ovmpt2df.4	. . . . . . 7 ⊢ ((φ ∧ (x = A ∧ y = B)) → ((A𝐹B) = 𝑅 → ψ))
38	36, 37	sylbid 139	. . . . . 6 ⊢ ((φ ∧ (x = A ∧ y = B)) → ((A𝐹B) = (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B) → ψ))
39	23, 38	syl5 28	. . . . 5 ⊢ ((φ ∧ (x = A ∧ y = B)) → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))
40	39	expr 357	. . . 4 ⊢ ((φ ∧ x = A) → (y = B → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)))
41	17, 22, 40	exlimd 1470	. . 3 ⊢ ((φ ∧ x = A) → (∃y y = B → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)))
42	16, 41	mpd 13	. 2 ⊢ ((φ ∧ x = A) → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))
43	1, 6, 11, 42	exlimdd 1734	1 ⊢ (φ → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1228  Ⅎwnf 1329  ∃wex 1362   ∈ wcel 1374  Ⅎwnfc 2147  Vcvv 2535  (class class class)co 5436   ↦ cmpt2 5438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918  ax-setind 4204

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-v 2537  df-sbc 2742  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-br 3739  df-opab 3793  df-id 4004  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-iota 4794  df-fun 4831  df-fv 4837  df-ov 5439  df-oprab 5440  df-mpt2 5441

This theorem is referenced by:  ovmpt2dv  5556  ovmpt2dv2  5557