Metamath Proof Explorer

Theorem trfr

Description: A transitive class well-founded by e. is a subclass of the class of well-founded sets. Part of Lemma I.9.21 of Kunen2 p. 53. (Contributed by Eric Schmidt, 26-Oct-2025)

Ref Expression
Assertion trfr ⊢ Tr ⁡ A ∧ E Fr A → A ⊆ ⋃ R1 On

Proof

Step Hyp Ref Expression
1 epse ⊢ E Se A
2 r19.21v ⊢ ∀ z ∈ Pred E A y Tr ⁡ A → z ∈ ⋃ R1 On ↔ Tr ⁡ A → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On
3 trpred ⊢ Tr ⁡ A ∧ y ∈ A → Pred E A y = y
4 raleq ⊢ Pred E A y = y → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On ↔ ∀ z ∈ y z ∈ ⋃ R1 On
5 dfss3 ⊢ y ⊆ ⋃ R1 On ↔ ∀ z ∈ y z ∈ ⋃ R1 On
6 4 5 bitr4di ⊢ Pred E A y = y → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On ↔ y ⊆ ⋃ R1 On
7 vex ⊢ y ∈ V
8 7 r1elss ⊢ y ∈ ⋃ R1 On ↔ y ⊆ ⋃ R1 On
9 6 8 bitr4di ⊢ Pred E A y = y → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On ↔ y ∈ ⋃ R1 On
10 3 9 syl ⊢ Tr ⁡ A ∧ y ∈ A → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On ↔ y ∈ ⋃ R1 On
11 10 biimpd ⊢ Tr ⁡ A ∧ y ∈ A → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On → y ∈ ⋃ R1 On
12 11 expcom ⊢ y ∈ A → Tr ⁡ A → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On → y ∈ ⋃ R1 On
13 12 a2d ⊢ y ∈ A → Tr ⁡ A → ∀ z ∈ Pred E A y z ∈ ⋃ R1 On → Tr ⁡ A → y ∈ ⋃ R1 On
14 2 13 biimtrid ⊢ y ∈ A → ∀ z ∈ Pred E A y Tr ⁡ A → z ∈ ⋃ R1 On → Tr ⁡ A → y ∈ ⋃ R1 On
15 eleq1w ⊢ y = z → y ∈ ⋃ R1 On ↔ z ∈ ⋃ R1 On
16 15 imbi2d ⊢ y = z → Tr ⁡ A → y ∈ ⋃ R1 On ↔ Tr ⁡ A → z ∈ ⋃ R1 On
17 14 16 frins2 ⊢ E Fr A ∧ E Se A → ∀ y ∈ A Tr ⁡ A → y ∈ ⋃ R1 On
18 1 17 mpan2 ⊢ E Fr A → ∀ y ∈ A Tr ⁡ A → y ∈ ⋃ R1 On
19 r19.21v ⊢ ∀ y ∈ A Tr ⁡ A → y ∈ ⋃ R1 On ↔ Tr ⁡ A → ∀ y ∈ A y ∈ ⋃ R1 On
20 18 19 sylib ⊢ E Fr A → Tr ⁡ A → ∀ y ∈ A y ∈ ⋃ R1 On
21 dfss3 ⊢ A ⊆ ⋃ R1 On ↔ ∀ y ∈ A y ∈ ⋃ R1 On
22 20 21 imbitrrdi ⊢ E Fr A → Tr ⁡ A → A ⊆ ⋃ R1 On
23 22 impcom ⊢ Tr ⁡ A ∧ E Fr A → A ⊆ ⋃ R1 On