Theorem fpwwe2lem2 10585

Description: Lemma for fpwwe2 10596. (Contributed by Mario Carneiro, 19-May-2015.) (Revised by AV, 20-Jul-2024.)

Hypotheses

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

Assertion

Ref	Expression
fpwwe2lem2	⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))

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

Allowed substitution hints:   𝐴(𝑦,𝑢)   𝑉(𝑥,𝑦,𝑢,𝑟)

Proof of Theorem fpwwe2lem2

Step	Hyp	Ref	Expression
1		fpwwe2.1	. . . . 5 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
2	1	relopabiv 5783	. . . 4 ⊢ Rel 𝑊
3	2	a1i 11	. . 3 ⊢ (𝜑 → Rel 𝑊)
4		brrelex12 5690	. . 3 ⊢ ((Rel 𝑊 ∧ 𝑋𝑊𝑅) → (𝑋 ∈ V ∧ 𝑅 ∈ V))
5	3, 4	sylan 580	. 2 ⊢ ((𝜑 ∧ 𝑋𝑊𝑅) → (𝑋 ∈ V ∧ 𝑅 ∈ V))
6		fpwwe2.2	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
7	6	adantr 480	. . . 4 ⊢ ((𝜑 ∧ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) → 𝐴 ∈ 𝑉)
8		simprll 778	. . . 4 ⊢ ((𝜑 ∧ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) → 𝑋 ⊆ 𝐴)
9	7, 8	ssexd 5279	. . 3 ⊢ ((𝜑 ∧ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) → 𝑋 ∈ V)
10	9, 9	xpexd 7727	. . . 4 ⊢ ((𝜑 ∧ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) → (𝑋 × 𝑋) ∈ V)
11		simprlr 779	. . . 4 ⊢ ((𝜑 ∧ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) → 𝑅 ⊆ (𝑋 × 𝑋))
12	10, 11	ssexd 5279	. . 3 ⊢ ((𝜑 ∧ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) → 𝑅 ∈ V)
13	9, 12	jca 511	. 2 ⊢ ((𝜑 ∧ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))) → (𝑋 ∈ V ∧ 𝑅 ∈ V))
14		simpl 482	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → 𝑥 = 𝑋)
15	14	sseq1d 3978	. . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴))
16		simpr 484	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅)
17	14	sqxpeqd 5670	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (𝑥 × 𝑥) = (𝑋 × 𝑋))
18	16, 17	sseq12d 3980	. . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (𝑟 ⊆ (𝑥 × 𝑥) ↔ 𝑅 ⊆ (𝑋 × 𝑋)))
19	15, 18	anbi12d 632	. . . 4 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ↔ (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋))))
20	16, 14	weeq12d 5627	. . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (𝑟 We 𝑥 ↔ 𝑅 We 𝑋))
21	16	cnveqd 5839	. . . . . . . 8 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → ◡𝑟 = ◡𝑅)
22	21	imaeq1d 6030	. . . . . . 7 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (◡𝑟 “ {𝑦}) = (◡𝑅 “ {𝑦}))
23	16	ineq1d 4182	. . . . . . . . 9 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (𝑟 ∩ (𝑢 × 𝑢)) = (𝑅 ∩ (𝑢 × 𝑢)))
24	23	oveq2d 7403	. . . . . . . 8 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = (𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))))
25	24	eqeq1d 2731	. . . . . . 7 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → ((𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))
26	22, 25	sbceqbid 3760	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → ([(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))
27	14, 26	raleqbidv 3319	. . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))
28	20, 27	anbi12d 632	. . . 4 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → ((𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦) ↔ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
29	19, 28	anbi12d 632	. . 3 ⊢ ((𝑥 = 𝑋 ∧ 𝑟 = 𝑅) → (((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦)) ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
30	29, 1	brabga 5494	. 2 ⊢ ((𝑋 ∈ V ∧ 𝑅 ∈ V) → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
31	5, 13, 30	pm5.21nd 801	1 ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3447  [wsbc 3753   ∩ cin 3913   ⊆ wss 3914  {csn 4589   class class class wbr 5107  {copab 5169   We wwe 5590   × cxp 5636  ^◡ccnv 5637   “ cima 5641  Rel wrel 5643  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  fpwwe2lem3  10586  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  canthwelem  10603  pwfseqlem4  10615