Theorem ovmpt2df 5534

Description: Alternate deduction version of ovmpt2 5538, 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 1404	. 2 ⊢ Ⅎxφ
2		ovmpt2df.5	. . . 4 ⊢ Ⅎx𝐹
3		nfmpt21 5473	. . . 4 ⊢ Ⅎx(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
4	2, 3	nfeq 2168	. . 3 ⊢ Ⅎx 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
5		ovmpt2df.6	. . 3 ⊢ Ⅎxψ
6	4, 5	nfim 1448	. 2 ⊢ Ⅎx(𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)
7		ovmpt2df.1	. . . 4 ⊢ (φ → A ∈ 𝐶)
8		elex 2542	. . . 4 ⊢ (A ∈ 𝐶 → A ∈ V)
9	7, 8	syl 14	. . 3 ⊢ (φ → A ∈ V)
10		isset 2538	. . 3 ⊢ (A ∈ V ↔ ∃x x = A)
11	9, 10	sylib 127	. 2 ⊢ (φ → ∃x x = A)
12		ovmpt2df.2	. . . . 5 ⊢ ((φ ∧ x = A) → B ∈ 𝐷)
13		elex 2542	. . . . 5 ⊢ (B ∈ 𝐷 → B ∈ V)
14	12, 13	syl 14	. . . 4 ⊢ ((φ ∧ x = A) → B ∈ V)
15		isset 2538	. . . 4 ⊢ (B ∈ V ↔ ∃y y = B)
16	14, 15	sylib 127	. . 3 ⊢ ((φ ∧ x = A) → ∃y y = B)
17		nfv 1404	. . . 4 ⊢ Ⅎy(φ ∧ x = A)
18		ovmpt2df.7	. . . . . 6 ⊢ Ⅎy𝐹
19		nfmpt22 5474	. . . . . 6 ⊢ Ⅎy(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
20	18, 19	nfeq 2168	. . . . 5 ⊢ Ⅎy 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
21		ovmpt2df.8	. . . . 5 ⊢ Ⅎyψ
22	20, 21	nfim 1448	. . . 4 ⊢ Ⅎy(𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)
23		oveq 5421	. . . . . 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 5433	. . . . . . . . 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 2097	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → x ∈ 𝐶)
29	12	adantrr 451	. . . . . . . . . . 11 ⊢ ((φ ∧ (x = A ∧ y = B)) → B ∈ 𝐷)
30	25, 29	eqeltrd 2097	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → y ∈ 𝐷)
31		ovmpt2df.3	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 ∈ 𝑉)
32		eqid 2023	. . . . . . . . . . 11 ⊢ (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
33	32	ovmpt4g 5525	. . . . . . . . . 10 ⊢ ((x ∈ 𝐶 ∧ y ∈ 𝐷 ∧ 𝑅 ∈ 𝑉) → (x(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)y) = 𝑅)
34	28, 30, 31, 33	syl3anc 1124	. . . . . . . . 9 ⊢ ((φ ∧ (x = A ∧ y = B)) → (x(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)y) = 𝑅)
35	26, 34	eqtr3d 2057	. . . . . . . 8 ⊢ ((φ ∧ (x = A ∧ y = B)) → (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B) = 𝑅)
36	35	eqeq2d 2034	. . . . . . 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 1472	. . 3 ⊢ ((φ ∧ x = A) → (∃y y = B → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)))
42	16, 41	mpd 13	. 2 ⊢ ((φ ∧ x = A) → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))
43	1, 6, 11, 42	exlimdd 1736	1 ⊢ (φ → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))

Syntax hints:   → wi 4   ∧ wa 97  Ⅎwnf 1329  ∃wex 1362   = wceq 1374   ∈ wcel 1376  Ⅎwnfc 2148  Vcvv 2534  (class class class)co 5415   ∈ cmpt2 5417

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 1378  ax-10 1379  ax-11 1380  ax-i12 1381  ax-bnd 1382  ax-4 1383  ax-14 1388  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-i5r 1412  ax-ext 2005  ax-sep 3828  ax-pow 3880  ax-pr 3897  ax-setind 4180

This theorem depends on definitions:  df-bi 110  df-3an 878  df-tru 1232  df-fal 1233  df-nf 1330  df-sb 1629  df-eu 1885  df-mo 1886  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-ne 2189  df-ral 2288  df-rex 2289  df-v 2536  df-sbc 2741  df-dif 2899  df-un 2901  df-in 2903  df-ss 2910  df-pw 3314  df-sn 3334  df-pr 3335  df-op 3337  df-uni 3534  df-br 3718  df-opab 3772  df-id 3984  df-xp 4254  df-rel 4255  df-cnv 4256  df-co 4257  df-dm 4258  df-iota 4771  df-fun 4808  df-fv 4814  df-ov 5418  df-oprab 5419  df-mpt2 5420

This theorem is referenced by:  ovmpt2dv  5535  ovmpt2dv2  5536