Theorem fpwwe2lem5 9713

Description: Lemma for fpwwe2 9722. (Contributed by Mario Carneiro, 15-May-2015.)

Hypotheses

Ref	Expression
fpwwe2.1	⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2	⊢ (𝜑 → 𝐴 ∈ V)
fpwwe2.3	⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)

Assertion

Ref	Expression
fpwwe2lem5	⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴)

Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑦,𝑢)

Proof of Theorem fpwwe2lem5

Step	Hyp	Ref	Expression
1		fpwwe2.2	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ V)
2	1	adantr 472	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝐴 ∈ V)
3		simpr1 1248	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑋 ⊆ 𝐴)
4	2, 3	ssexd 4968	. . 3 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑋 ∈ V)
5		xpexg 7162	. . . . 5 ⊢ ((𝑋 ∈ V ∧ 𝑋 ∈ V) → (𝑋 × 𝑋) ∈ V)
6	4, 4, 5	syl2anc 579	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋 × 𝑋) ∈ V)
7		simpr2 1250	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑅 ⊆ (𝑋 × 𝑋))
8	6, 7	ssexd 4968	. . 3 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → 𝑅 ∈ V)
9	4, 8	jca 507	. 2 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋 ∈ V ∧ 𝑅 ∈ V))
10		sseq1 3788	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴))
11		xpeq12 5304	. . . . . . . 8 ⊢ ((𝑥 = 𝑋 ∧ 𝑥 = 𝑋) → (𝑥 × 𝑥) = (𝑋 × 𝑋))
12	11	anidms 562	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 × 𝑥) = (𝑋 × 𝑋))
13	12	sseq2d 3795	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑟 ⊆ (𝑋 × 𝑋)))
14		weeq2 5268	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑟 We 𝑥 ↔ 𝑟 We 𝑋))
15	10, 13, 14	3anbi123d 1560	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) ↔ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)))
16	15	anbi2d 622	. . . 4 ⊢ (𝑥 = 𝑋 → ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) ↔ (𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋))))
17		oveq1 6853	. . . . 5 ⊢ (𝑥 = 𝑋 → (𝑥𝐹𝑟) = (𝑋𝐹𝑟))
18	17	eleq1d 2829	. . . 4 ⊢ (𝑥 = 𝑋 → ((𝑥𝐹𝑟) ∈ 𝐴 ↔ (𝑋𝐹𝑟) ∈ 𝐴))
19	16, 18	imbi12d 335	. . 3 ⊢ (𝑥 = 𝑋 → (((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)) → (𝑋𝐹𝑟) ∈ 𝐴)))
20		sseq1 3788	. . . . . 6 ⊢ (𝑟 = 𝑅 → (𝑟 ⊆ (𝑋 × 𝑋) ↔ 𝑅 ⊆ (𝑋 × 𝑋)))
21		weeq1 5267	. . . . . 6 ⊢ (𝑟 = 𝑅 → (𝑟 We 𝑋 ↔ 𝑅 We 𝑋))
22	20, 21	3anbi23d 1563	. . . . 5 ⊢ (𝑟 = 𝑅 → ((𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋) ↔ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)))
23	22	anbi2d 622	. . . 4 ⊢ (𝑟 = 𝑅 → ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)) ↔ (𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋))))
24		oveq2 6854	. . . . 5 ⊢ (𝑟 = 𝑅 → (𝑋𝐹𝑟) = (𝑋𝐹𝑅))
25	24	eleq1d 2829	. . . 4 ⊢ (𝑟 = 𝑅 → ((𝑋𝐹𝑟) ∈ 𝐴 ↔ (𝑋𝐹𝑅) ∈ 𝐴))
26	23, 25	imbi12d 335	. . 3 ⊢ (𝑟 = 𝑅 → (((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑋 × 𝑋) ∧ 𝑟 We 𝑋)) → (𝑋𝐹𝑟) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴)))
27		fpwwe2.3	. . 3 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
28	19, 26, 27	vtocl2g 3422	. 2 ⊢ ((𝑋 ∈ V ∧ 𝑅 ∈ V) → ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴))
29	9, 28	mpcom 38	1 ⊢ ((𝜑 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋) ∧ 𝑅 We 𝑋)) → (𝑋𝐹𝑅) ∈ 𝐴)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1107   = wceq 1652   ∈ wcel 2155  ∀wral 3055  Vcvv 3350  [wsbc 3598   ∩ cin 3733   ⊆ wss 3734  {csn 4336  {copab 4873   We wwe 5237   × cxp 5277  ^◡ccnv 5278   “ cima 5282  (class class class)co 6846

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-op 4343  df-uni 4597  df-br 4812  df-opab 4874  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-iota 6033  df-fv 6078  df-ov 6849

This theorem is referenced by:  fpwwe2lem13  9721