Theorem ovmpt2df 5574

Description: Alternate deduction version of ovmpt2 5578, 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 1418	. 2 ⊢ Ⅎxφ
2		ovmpt2df.5	. . . 4 ⊢ Ⅎx𝐹
3		nfmpt21 5513	. . . 4 ⊢ Ⅎx(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
4	2, 3	nfeq 2182	. . 3 ⊢ Ⅎx 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
5		ovmpt2df.6	. . 3 ⊢ Ⅎxψ
6	4, 5	nfim 1461	. 2 ⊢ Ⅎx(𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)
7		ovmpt2df.1	. . . 4 ⊢ (φ → A ∈ 𝐶)
8		elex 2560	. . . 4 ⊢ (A ∈ 𝐶 → A ∈ V)
9	7, 8	syl 14	. . 3 ⊢ (φ → A ∈ V)
10		isset 2555	. . 3 ⊢ (A ∈ V ↔ ∃x x = A)
11	9, 10	sylib 127	. 2 ⊢ (φ → ∃x x = A)
12		ovmpt2df.2	. . . . 5 ⊢ ((φ ∧ x = A) → B ∈ 𝐷)
13		elex 2560	. . . . 5 ⊢ (B ∈ 𝐷 → B ∈ V)
14	12, 13	syl 14	. . . 4 ⊢ ((φ ∧ x = A) → B ∈ V)
15		isset 2555	. . . 4 ⊢ (B ∈ V ↔ ∃y y = B)
16	14, 15	sylib 127	. . 3 ⊢ ((φ ∧ x = A) → ∃y y = B)
17		nfv 1418	. . . 4 ⊢ Ⅎy(φ ∧ x = A)
18		ovmpt2df.7	. . . . . 6 ⊢ Ⅎy𝐹
19		nfmpt22 5514	. . . . . 6 ⊢ Ⅎy(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
20	18, 19	nfeq 2182	. . . . 5 ⊢ Ⅎy 𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
21		ovmpt2df.8	. . . . 5 ⊢ Ⅎyψ
22	20, 21	nfim 1461	. . . 4 ⊢ Ⅎy(𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)
23		oveq 5461	. . . . . 6 ⊢ (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → (A𝐹B) = (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B))
24		simprl 483	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → x = A)
25		simprr 484	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → y = B)
26	24, 25	oveq12d 5473	. . . . . . . . 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 2111	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → x ∈ 𝐶)
29	12	adantrr 448	. . . . . . . . . . 11 ⊢ ((φ ∧ (x = A ∧ y = B)) → B ∈ 𝐷)
30	25, 29	eqeltrd 2111	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → y ∈ 𝐷)
31		ovmpt2df.3	. . . . . . . . . 10 ⊢ ((φ ∧ (x = A ∧ y = B)) → 𝑅 ∈ 𝑉)
32		eqid 2037	. . . . . . . . . . 11 ⊢ (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)
33	32	ovmpt4g 5565	. . . . . . . . . 10 ⊢ ((x ∈ 𝐶 ∧ y ∈ 𝐷 ∧ 𝑅 ∈ 𝑉) → (x(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)y) = 𝑅)
34	28, 30, 31, 33	syl3anc 1134	. . . . . . . . 9 ⊢ ((φ ∧ (x = A ∧ y = B)) → (x(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)y) = 𝑅)
35	26, 34	eqtr3d 2071	. . . . . . . 8 ⊢ ((φ ∧ (x = A ∧ y = B)) → (A(x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅)B) = 𝑅)
36	35	eqeq2d 2048	. . . . . . 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 1485	. . 3 ⊢ ((φ ∧ x = A) → (∃y y = B → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ)))
42	16, 41	mpd 13	. 2 ⊢ ((φ ∧ x = A) → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))
43	1, 6, 11, 42	exlimdd 1749	1 ⊢ (φ → (𝐹 = (x ∈ 𝐶, y ∈ 𝐷 ↦ 𝑅) → ψ))

Syntax hints:   → wi 4   ∧ wa 97   = wceq 1242  Ⅎwnf 1346  ∃wex 1378   ∈ wcel 1390  Ⅎwnfc 2162  Vcvv 2551  (class class class)co 5455   ↦ cmpt2 5457

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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-setind 4220

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-iota 4810  df-fun 4847  df-fv 4853  df-ov 5458  df-oprab 5459  df-mpt2 5460

This theorem is referenced by:  ovmpt2dv  5575  ovmpt2dv2  5576