f1omoOLD

Description: Obsolete version of f1omo as of 24-Nov-2025. (Contributed by Zhi Wang, 19-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	f1omo.1	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 1_o } ) )
	Assertion	f1omoOLD	⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		f1omo.1	⊢ ( 𝜑 → 𝐹 = ( 𝐴 × { 1_o } ) )
2		1oex	⊢ 1_o ∈ V
3		eqid	⊢ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = ( ( 𝐴 × { 1_o } ) ‘ 𝑋 )
4	2 3	fvconst0ci	⊢ ( ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = 1_o )
5		mo0	⊢ ( ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = ∅ → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) )
6		el1o	⊢ ( 𝑦 ∈ 1_o ↔ 𝑦 = ∅ )
7		el1o	⊢ ( 𝑥 ∈ 1_o ↔ 𝑥 = ∅ )
8		eqtr3	⊢ ( ( 𝑦 = ∅ ∧ 𝑥 = ∅ ) → 𝑦 = 𝑥 )
9	6 7 8	syl2anb	⊢ ( ( 𝑦 ∈ 1_o ∧ 𝑥 ∈ 1_o ) → 𝑦 = 𝑥 )
10	9	gen2	⊢ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 1_o ∧ 𝑥 ∈ 1_o ) → 𝑦 = 𝑥 )
11		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 1_o ↔ 𝑥 ∈ 1_o ) )
12	11	mo4	⊢ ( ∃* 𝑦 𝑦 ∈ 1_o ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 1_o ∧ 𝑥 ∈ 1_o ) → 𝑦 = 𝑥 ) )
13	10 12	mpbir	⊢ ∃* 𝑦 𝑦 ∈ 1_o
14		eleq2w2	⊢ ( ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = 1_o → ( 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) ↔ 𝑦 ∈ 1_o ) )
15	14	mobidv	⊢ ( ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = 1_o → ( ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) ↔ ∃* 𝑦 𝑦 ∈ 1_o ) )
16	13 15	mpbiri	⊢ ( ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = 1_o → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) )
17	5 16	jaoi	⊢ ( ( ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = ∅ ∨ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) = 1_o ) → ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) )
18	4 17	ax-mp	⊢ ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 )
19	1	fveq1d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) )
20	19	eleq2d	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) ) )
21	20	mobidv	⊢ ( 𝜑 → ( ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ∃* 𝑦 𝑦 ∈ ( ( 𝐴 × { 1_o } ) ‘ 𝑋 ) ) )
22	18 21	mpbiri	⊢ ( 𝜑 → ∃* 𝑦 𝑦 ∈ ( 𝐹 ‘ 𝑋 ) )

Metamath Proof Explorer

Theorem f1omoOLD

Proof