Theorem weiunfrlem

Description: Lemma for weiunfr . (Contributed by Matthew House, 23-Aug-2025)

	Ref	Expression
Hypotheses	weiun.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
	weiun.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
	weiunlem2.3	⊢ ( 𝜑 → 𝑅 We 𝐴 )
	weiunlem2.4	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
	weiunfrlem.5	⊢ 𝐸 = ( ℩ 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 )
	weiunfrlem.6	⊢ ( 𝜑 → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
	weiunfrlem.7	⊢ ( 𝜑 → 𝑟 ≠ ∅ )
Assertion	weiunfrlem	⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑡 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ( 𝐹 ‘ 𝑡 ) = 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		weiun.1	⊢ 𝐹 = ( 𝑤 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↦ ( ℩ 𝑢 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ∀ 𝑣 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑤 ∈ 𝐵 } ¬ 𝑣 𝑅 𝑢 ) )
2		weiun.2	⊢ 𝑇 = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑦 ) 𝑅 ( 𝐹 ‘ 𝑧 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 ⦋ ( 𝐹 ‘ 𝑦 ) / 𝑥 ⦌ 𝑆 𝑧 ) ) ) }
3		weiunlem2.3	⊢ ( 𝜑 → 𝑅 We 𝐴 )
4		weiunlem2.4	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
5		weiunfrlem.5	⊢ 𝐸 = ( ℩ 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 )
6		weiunfrlem.6	⊢ ( 𝜑 → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
7		weiunfrlem.7	⊢ ( 𝜑 → 𝑟 ≠ ∅ )
8	1 2 3 4	weiunlem2	⊢ ( 𝜑 → ( 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑡 ∈ ⦋ ( 𝐹 ‘ 𝑡 ) / 𝑥 ⦌ 𝐵 ∧ ∀ 𝑠 ∈ 𝐴 ∀ 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ) )
9	8	simp1d	⊢ ( 𝜑 → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
10	9	fimassd	⊢ ( 𝜑 → ( 𝐹 “ 𝑟 ) ⊆ 𝐴 )
11	9	fdmd	⊢ ( 𝜑 → dom 𝐹 = ∪ 𝑥 ∈ 𝐴 𝐵 )
12	6 11	sseqtrrd	⊢ ( 𝜑 → 𝑟 ⊆ dom 𝐹 )
13		sseqin2	⊢ ( 𝑟 ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ 𝑟 ) = 𝑟 )
14	12 13	sylib	⊢ ( 𝜑 → ( dom 𝐹 ∩ 𝑟 ) = 𝑟 )
15	14 7	eqnetrd	⊢ ( 𝜑 → ( dom 𝐹 ∩ 𝑟 ) ≠ ∅ )
16	15	imadisjlnd	⊢ ( 𝜑 → ( 𝐹 “ 𝑟 ) ≠ ∅ )
17		wereu2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ( 𝐹 “ 𝑟 ) ⊆ 𝐴 ∧ ( 𝐹 “ 𝑟 ) ≠ ∅ ) ) → ∃! 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 )
18	3 4 10 16 17	syl22anc	⊢ ( 𝜑 → ∃! 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 )
19		riotacl2	⊢ ( ∃! 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 → ( ℩ 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∈ { 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 } )
20	18 19	syl	⊢ ( 𝜑 → ( ℩ 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 ) ∈ { 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 } )
21		simpr	⊢ ( ( 𝑛 = 𝑝 ∧ 𝑜 = 𝑞 ) → 𝑜 = 𝑞 )
22		simpl	⊢ ( ( 𝑛 = 𝑝 ∧ 𝑜 = 𝑞 ) → 𝑛 = 𝑝 )
23	21 22	breq12d	⊢ ( ( 𝑛 = 𝑝 ∧ 𝑜 = 𝑞 ) → ( 𝑜 𝑅 𝑛 ↔ 𝑞 𝑅 𝑝 ) )
24	23	notbid	⊢ ( ( 𝑛 = 𝑝 ∧ 𝑜 = 𝑞 ) → ( ¬ 𝑜 𝑅 𝑛 ↔ ¬ 𝑞 𝑅 𝑝 ) )
25	24	cbvraldva	⊢ ( 𝑛 = 𝑝 → ( ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝑛 ↔ ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 ) )
26	25	cbvrabv	⊢ { 𝑛 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝑛 } = { 𝑝 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑞 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑞 𝑅 𝑝 }
27	20 5 26	3eltr4g	⊢ ( 𝜑 → 𝐸 ∈ { 𝑛 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝑛 } )
28		breq2	⊢ ( 𝑛 = 𝐸 → ( 𝑜 𝑅 𝑛 ↔ 𝑜 𝑅 𝐸 ) )
29	28	notbid	⊢ ( 𝑛 = 𝐸 → ( ¬ 𝑜 𝑅 𝑛 ↔ ¬ 𝑜 𝑅 𝐸 ) )
30	29	ralbidv	⊢ ( 𝑛 = 𝐸 → ( ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝑛 ↔ ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝐸 ) )
31	30	elrab	⊢ ( 𝐸 ∈ { 𝑛 ∈ ( 𝐹 “ 𝑟 ) ∣ ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝑛 } ↔ ( 𝐸 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝐸 ) )
32	27 31	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝐸 ) )
33	32	simpld	⊢ ( 𝜑 → 𝐸 ∈ ( 𝐹 “ 𝑟 ) )
34	32	simprd	⊢ ( 𝜑 → ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝐸 )
35	9	ffnd	⊢ ( 𝜑 → 𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵 )
36		breq1	⊢ ( 𝑜 = ( 𝐹 ‘ 𝑡 ) → ( 𝑜 𝑅 𝐸 ↔ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ) )
37	36	notbid	⊢ ( 𝑜 = ( 𝐹 ‘ 𝑡 ) → ( ¬ 𝑜 𝑅 𝐸 ↔ ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ) )
38	37	ralima	⊢ ( ( 𝐹 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝐸 ↔ ∀ 𝑡 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ) )
39	35 6 38	syl2anc	⊢ ( 𝜑 → ( ∀ 𝑜 ∈ ( 𝐹 “ 𝑟 ) ¬ 𝑜 𝑅 𝐸 ↔ ∀ 𝑡 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ) )
40	34 39	mpbid	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 )
41		simpr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) )
42	41	elin1d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝑡 ∈ 𝑟 )
43		rspa	⊢ ( ( ∀ 𝑡 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ∧ 𝑡 ∈ 𝑟 ) → ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 )
44	40 42 43	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 )
45		csbeq1	⊢ ( 𝑠 = 𝐸 → ⦋ 𝑠 / 𝑥 ⦌ 𝐵 = ⦋ 𝐸 / 𝑥 ⦌ 𝐵 )
46		breq1	⊢ ( 𝑠 = 𝐸 → ( 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ↔ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) ) )
47	46	notbid	⊢ ( 𝑠 = 𝐸 → ( ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ↔ ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) ) )
48	45 47	raleqbidv	⊢ ( 𝑠 = 𝐸 → ( ∀ 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) ) )
49	8	simp3d	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝐴 ∀ 𝑡 ∈ ⦋ 𝑠 / 𝑥 ⦌ 𝐵 ¬ 𝑠 𝑅 ( 𝐹 ‘ 𝑡 ) )
50	10 33	sseldd	⊢ ( 𝜑 → 𝐸 ∈ 𝐴 )
51	48 49 50	rspcdva	⊢ ( 𝜑 → ∀ 𝑡 ∈ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) )
52	41	elin2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝑡 ∈ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 )
53		rspa	⊢ ( ( ∀ 𝑡 ∈ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) ∧ 𝑡 ∈ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) → ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) )
54	51 52 53	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) )
55		weso	⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
56	3 55	syl	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
57	56	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝑅 Or 𝐴 )
58	9	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ 𝐴 )
59	6	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝑟 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
60	59 42	sseldd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝑡 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
61	58 60	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ 𝐴 )
62	50	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → 𝐸 ∈ 𝐴 )
63		sotrieq2	⊢ ( ( 𝑅 Or 𝐴 ∧ ( ( 𝐹 ‘ 𝑡 ) ∈ 𝐴 ∧ 𝐸 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑡 ) = 𝐸 ↔ ( ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ∧ ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) )
64	57 61 62 63	syl12anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑡 ) = 𝐸 ↔ ( ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ∧ ¬ 𝐸 𝑅 ( 𝐹 ‘ 𝑡 ) ) ) )
65	44 54 64	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ) → ( 𝐹 ‘ 𝑡 ) = 𝐸 )
66	65	ralrimiva	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ( 𝐹 ‘ 𝑡 ) = 𝐸 )
67	33 40 66	3jca	⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝐹 “ 𝑟 ) ∧ ∀ 𝑡 ∈ 𝑟 ¬ ( 𝐹 ‘ 𝑡 ) 𝑅 𝐸 ∧ ∀ 𝑡 ∈ ( 𝑟 ∩ ⦋ 𝐸 / 𝑥 ⦌ 𝐵 ) ( 𝐹 ‘ 𝑡 ) = 𝐸 ) )